Theorems · Inductive type · nonassociative algebras
IsCommJordan
(A : Type u_1) → [CommMagma A] → Prop
A commutative Jordan multiplication
- Defined in
- Mathlib.Algebra.Jordan.Basic
- Cited by
- 3 results in Mathlib
- Foundations
- Depth 1 from the axioms · uses no axioms
- Assumes
- CommMagma
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites1
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- CommMagmastatement · cited by 57
Cited by5
Results whose statement or proof uses this declaration.
- two_nsmul_lie_lmul_lmul_add_add_eq_zerostatement and proof · cited by 0
- two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_addstatement and proof · cited by 0
- IsCommJordan.casesOnstatement and proof · cited by 0
- IsCommJordan.lmul_comm_rmul_rmulstatement and proof · cited by 0
- IsCommJordan.recOnstatement and proof · cited by 0