mathlib3
feat(algebra/jordan/triple): Introduce Jordan triples
#11553
Open
Overview
Commits
49
Changes
View On GitHub

feat(algebra/jordan/triple): Introduce Jordan triples #11553

mans0954 wants to merge 49 commits into master from jordan-triples
mans0954
mans0954 Start defining triple product
ed6c9311
mans0954 Add dub lemmas
485316d0
mans0954 Introduce D(a,b) operator
ade88e28
mans0954 Show D additive in each variable
28111991
mans0954 Show the D(a,b) operator is Lebnitz
6c365574
mans0954 use a\_1 a\_2 etc in addition
7b94e971
mans0954 More consistant spacing
41cd0087
mans0954 Define Q operator
cb1f4412
mans0954 Typo
182fe99a
mans0954 Remove unnecessary imports
220bdf33
mans0954 Add some documentation
91c2d176
mans0954 Normalise references
546e159e
mans0954 Add references
fc31d1ad
mans0954 misformatting of curly braces
c518b694
mans0954 Linter says defs not lemmas
6d3dc6d2
mans0954 Fix issue with lebintz def
b90d2dec
mans0954 mans0954 added awaiting-review
eric-wieser
eric-wieser commented on 2022-01-19
eric-wieser
eric-wieser commented on 2022-01-19
eric-wieser eric-wieser removed awaiting-review
eric-wieser eric-wieser added awaiting-author
YaelDillies
YaelDillies commented on 2022-01-19
eric-wieser
eric-wieser commented on 2022-01-19
mans0954 Spell "Leibniz" correctly
0630421b
mans0954 Update src/algebra/jordan/triple.lean
802a1407
mans0954 gsmul -> zsmul
a3eb7947
mans0954 Redefine D
1e7198b9
mans0954 Redefine Q
f12f78ff
mans0954 Shorten proofs
828fd103
mans0954 misformatting of curly braces
fc7320b7
mans0954 Add missing docstrings
a80872af
mans0954 mans0954 removed awaiting-author
mans0954 mans0954 added awaiting-review
eric-wieser
eric-wieser commented on 2022-01-20
eric-wieser
eric-wieser commented on 2022-01-20
mans0954 Shorten add_monoid_hom.tp
5bb62f26
mans0954 Closing brackets
49d50e43
mans0954 Remove Q'
385d3b0c
eric-wieser
eric-wieser commented on 2022-01-20
eric-wieser eric-wieser removed awaiting-review
eric-wieser eric-wieser added awaiting-author
eric-wieser
eric-wieser commented on 2022-01-20
mans0954 Update src/algebra/jordan/triple.lean
276386c9
mans0954 Remove "by exact"
83902365
mans0954 Introduce trilinear products
f4e01f40
mans0954 Merge branch 'ternary' into jordan-triples
50f0a4d4
mans0954 Add add_monoid_hom.tp
737ec431
mans0954 Merge branch 'ternary' into jordan-triples
2e53655a
mans0954 Import ternary
0c939d66
mans0954 Shorten lines
a598d3f0
leanprover-community-bot-assistant leanprover-community-bot-assistant added blocked-by-other-PR
YaelDillies
YaelDillies commented on 2022-01-21
mans0954
leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict
mans0954 Merge branch 'master' into jordan-triples
626e74ed
leanprover-community-bot-assistant leanprover-community-bot-assistant removed merge-conflict
mans0954
mans0954 Rework definition of triple product
1e879695
mans0954 Lint
bff64349
mans0954 Remove ternary file
631a0fc8
leanprover-community-bot-assistant leanprover-community-bot-assistant removed blocked-by-other-PR
mans0954
eric-wieser
eric-wieser commented on 2022-02-03
eric-wieser
eric-wieser commented on 2022-02-03
eric-wieser
eric-wieser commented on 2022-02-03
eric-wieser
eric-wieser commented on 2022-02-03
eric-wieser
eric-wieser commented on 2022-02-03
eric-wieser
eric-wieser commented on 2022-02-03
YaelDillies
YaelDillies commented on 2022-02-03
mans0954 Update src/algebra/jordan/triple.lean
54e35ce7
mans0954 Replace proof with rfl
55462aaf
mans0954 Update src/algebra/jordan/triple.lean
e8bfb712
mans0954 Replace Q_def proof with rfl
9d3a2158
mans0954 Remove lemmas relating to expanding bilinear products
27d5ab69
mans0954 Rename and reorganise things a bit
a263b479
mans0954 Use add_comm_group instead of add_comm_monoid and has_sub
5663a3ff
leanprover-community-bot-assistant leanprover-community-bot-assistant added merge-conflict
YaelDillies Merge branch 'master' into jordan-triples
f0af9c53
YaelDillies fix merge accident
05b8da86
kim-em kim-em added too-late
mans0954 Merge branch 'master' into jordan-triples
1914bfa3

Login to write a write a comment.

Login via GitHub

Reviewers
Assignees
No one assigned
Labels
awaiting-author too-late
Milestone
No milestone
Terms Of Use Privacy Policy Refund Policy Impressum