feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings #16094

artie2000 · 2024-08-23T12:59:01Z

Generalise definition of a semireal ring, as discussed at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Formally.20real.20fields
Add facts about multiplicative structure of sums of squares -- preserved under multiplication, form a semiring, set of sums of squares is the semiring generated by the squares.
Update documentation

Deletions:

mem_sumSq_of_isSquare (statement changed to IsSquare.isSumSq)

This is work towards formalising some real algebra (see https://github.com/artie2000/real_closed_field).

depends on: [Merged by Bors] - feat(Algebra): add missing substructure lemmas #20269
depends on: [Merged by Bors] - chore(Algebra): rename theorems for consistency #20271
depends on: [Merged by Bors] - feat(Algebra/Group/Even): "Advanced" lemmas about even elements. #20272
depends on: [Merged by Bors] - chore(Algebra): make more names consistent #20449
depends on: [Merged by Bors] - chore(Algebra): Improve attribute generation #20451
depends on: chore(Subalgebra/Unitization): move unrelated defs/lemmas earlier #20526
depends on: [Merged by Bors] - chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs #20528

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

…munity/mathlib4 into real_closed_field

) * Make documentation clearer and more concise * Make notation consistent * Make proofs cleaner This PR splits off yet more chore material from #16094 Moves: * `sumSq` -> `AddSubmonoid.sumSq`

artie2000 and others added 30 commits August 19, 2024 13:35

Rewrote Order.group.Cone to be based on the substructure pattern.

b2b1bdd

Add inherited instances

ec01c52

Update documentation + add reverse constructions

910bc2f

Update Mathlib/Algebra/Order/Group/Cone.lean

e0fdbf8

Co-authored-by: github-actions[bot] <41898282+github-actions[bot]@users.noreply.github.com>

more work

55d74d9

Merge branch 'real_closed_field' of https://github.com/leanprover-com…

8ae9a21

…munity/mathlib4 into real_closed_field

update

919a93f

missing simp lemmas

bbb7865

more work on rings

844e8e6

first nontrivial proof!

347e8c5

fixing mkOf

e78cbd2

positivity test

860bd1d

hotfix definition

b0dac72

zerzer

d6afdda

for pull

9b95b24

Merge branch 'real_closed_field' of https://github.com/leanprover-com…

ca32cb2

…munity/mathlib4 into real_closed_field

finish fixing ring cone

6e9cf21

sum of squares stuff

4eaaf0f

final content amount

20e6e65

fix build

9092291

changes based on feedback

490f196

add multiplicative versions

f0dae6b

docstrings

b38ee18

fix namespaces

a53848e

Generalise definition

5fa2878

improve documentation

c0238c4

docs

4ccca47

change definition according to feedback

a5bf7ba

fix to_additive style

e4d5e9a

typo

93f78cc

artie2000 added 4 commits January 6, 2025 19:54

improve docs

1190ebc

sync

f101491

fix

a9a7dce

style

ad2ba3a

YaelDillies mentioned this pull request Jan 6, 2025

chore(Subalgebra/Unitization): move unrelated defs/lemmas earlier #20526

Open

artie2000 mentioned this pull request Jan 6, 2025

[Merged by Bors] - chore(Algebra/Ring): Clean up in SumsOfSquares and Semireal/Defs #20528

Closed

remove spurious deprecation

29d9631

mathlib4-dependent-issues-bot added the blocked-by-other-PR This PR depends on another PR to Mathlib (this label is automatically managed by a bot) label Jan 6, 2025

artie2000 added 6 commits January 6, 2025 20:36

sync

d0a4b98

style

7cc36d2

fix

bf2a090

docs

56c64c5

fix typo

72f6efa

fix typo

2da9105

artie2000 removed the awaiting-author A reviewer has asked the author a question or requested changes label Jan 6, 2025

artie2000 added 2 commits January 6, 2025 21:50

remove extra import

03c8b03

sync style

7e6890c

artie2000 added 12 commits January 7, 2025 18:08

Merge branch 'master' into real_closed_field_dev

e7c2293

docs

e268231

fix naming

ba72430

fix naming

7561ff8

fix merge issues

4ad9460

fix merge issue

ead992b

fix explicit

9df4ae0

restore deprecation

a60d2a1

sync

9611f41

optimise names

62fbdde

make sure IsSumSq 0 is provable by aesop

c0a6ebe

revert test

529f9c4

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings #16094

feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings #16094

artie2000 commented Aug 23, 2024 •

edited

Loading

feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings #16094

Are you sure you want to change the base?

feat(Algebra/Ring): generalise and extend material about sums of squares and semireal rings #16094

Conversation

artie2000 commented Aug 23, 2024 • edited Loading

artie2000 commented Aug 23, 2024 •

edited

Loading