Basic

📁 Source: Mathlib/Algebra/Jordan/Basic.lean

Statistics

Metric	Count
Definitions IsCommJordan, IsJordan	2
Theorems isCommJordan, lmul_comm_rmul_rmul, toIsJordan, lmul_comm_rmul, lmul_comm_rmul_rmul, lmul_lmul_comm_lmul, lmul_lmul_comm_rmul, rmul_comm_rmul_rmul, isJordan, commute_lmul_lmul_sq, commute_lmul_rmul, commute_lmul_rmul_sq, commute_lmul_sq_rmul, commute_rmul_rmul_sq, two_nsmul_lie_lmul_lmul_add_add_eq_zero, two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add	16
Total	18

CommSemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCommJordan 📖	mathematical	—	IsCommJordan toCommMagma	—	mul_assoc

IsCommJordan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lmul_comm_rmul_rmul 📖	mathematical	—	CommMagma.toMul	—	—
toIsJordan 📖	mathematical	—	IsJordan CommMagma.toMul	—	mul_comm lmul_comm_rmul_rmul

IsJordan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
lmul_comm_rmul 📖	—	—	—	—	—
lmul_comm_rmul_rmul 📖	—	—	—	—	—
lmul_lmul_comm_lmul 📖	—	—	—	—	—
lmul_lmul_comm_rmul 📖	—	—	—	—	—
rmul_comm_rmul_rmul 📖	—	—	—	—	—

Semigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isJordan 📖	mathematical	—	IsJordan toMul	—	mul_assoc

(root)

Definitions

Name	Category	Theorems
IsCommJordan 📖	CompData	2 math math: CommSemigroup.isCommJordan, SymAlg.instIsCommJordan
IsJordan 📖	CompData	2 math math: Semigroup.isJordan, IsCommJordan.toIsJordan

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
commute_lmul_lmul_sq 📖	mathematical	—	Commute AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddMonoid.End.instMul DFunLike.coe AddMonoidHom AddMonoid.End.instAddCommMonoid AddMonoidHom.instFunLike AddMonoid.End.mulLeft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	AddMonoidHom.ext IsJordan.lmul_lmul_comm_lmul
commute_lmul_rmul 📖	mathematical	—	Commute AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddMonoid.End.instMul DFunLike.coe AddMonoidHom AddMonoid.End.instAddCommMonoid AddMonoidHom.instFunLike AddMonoid.End.mulLeft AddMonoid.End.mulRight	—	AddMonoidHom.ext IsJordan.lmul_comm_rmul
commute_lmul_rmul_sq 📖	mathematical	—	Commute AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddMonoid.End.instMul DFunLike.coe AddMonoidHom AddMonoid.End.instAddCommMonoid AddMonoidHom.instFunLike AddMonoid.End.mulLeft AddMonoid.End.mulRight Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	AddMonoidHom.ext IsJordan.lmul_comm_rmul_rmul
commute_lmul_sq_rmul 📖	mathematical	—	Commute AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddMonoid.End.instMul DFunLike.coe AddMonoidHom AddMonoid.End.instAddCommMonoid AddMonoidHom.instFunLike AddMonoid.End.mulLeft Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoid.End.mulRight	—	AddMonoidHom.ext IsJordan.lmul_lmul_comm_rmul
commute_rmul_rmul_sq 📖	mathematical	—	Commute AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring AddMonoid.End.instMul DFunLike.coe AddMonoidHom AddMonoid.End.instAddCommMonoid AddMonoidHom.instFunLike AddMonoid.End.mulRight Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	AddMonoidHom.ext IsJordan.rmul_comm_rmul_rmul
two_nsmul_lie_lmul_lmul_add_add_eq_zero 📖	mathematical	—	AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddMonoid.End.instAddMonoidWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoid.End.instRing NonUnitalNonAssocRing.toAddCommGroup Bracket.bracket LieRingModule.toBracket LieRing.ofAssociativeRing LieRing.toAddCommGroup lieRingSelfModule DFunLike.coe AddMonoidHom AddMonoid.End.instAddCommMonoid AddMonoidHom.instFunLike AddMonoid.End.mulLeft Distrib.toMul MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Commute.lie_eq commute_lmul_lmul_sq IsCommJordan.toIsJordan nsmul_add
two_nsmul_lie_lmul_lmul_add_eq_lie_lmul_lmul_add 📖	mathematical	—	AddMonoid.End AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddMonoid.End.instAddMonoidWithOne Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing AddMonoid.End.instRing NonUnitalNonAssocRing.toAddCommGroup Bracket.bracket LieRingModule.toBracket LieRing.ofAssociativeRing LieRing.toAddCommGroup lieRingSelfModule DFunLike.coe AddMonoidHom AddMonoid.End.instAddCommMonoid AddMonoidHom.instFunLike AddMonoid.End.mulLeft Distrib.toMul	—	two_smul mul_comm map_add AddMonoidHomClass.toAddHomClass AddMonoidHom.instAddMonoidHomClass mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass lie_add add_lie Commute.lie_eq commute_lmul_lmul_sq IsCommJordan.toIsJordan zero_add add_zero Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Tactic.Abel.term_add_constg Mathlib.Tactic.Abel.const_add_termg sub_eq_zero sub_sub sub_eq_add_neg lie_skew nsmul_add

---

← Back to Index