Symmetrized

📁 Source: Mathlib/Algebra/Symmetrized.lean

Statistics

Metric	Count
Definitions `SymAlg`, `addCommGroup`, `addCommMonoid`, `addCommSemigroup`, `addGroup`, `addMonoid`, `instAdd`, `instCommMagmaOfInvertibleOfNat`, `instInhabited`, `instInv`, `instInvertibleCoeEquivSym`, `instModule`, `instMulOfAddOfInvertibleOfNat`, `instNeg`, `instNonAssocRingOfInvertibleOfNat`, `instOne`, `instSMul`, `instSub`, `instUnique`, `instZero`, `nonAssocSemiring`, `sym`, `unsym`, `«term_ˢʸᵐ»`	24
Theorems `instIsCommJordan`, `instIsEmpty`, `instNontrivial`, `instSubsingleton`, `invOf_sym`, `mul_comm`, `mul_def`, `sym_add`, `sym_bijective`, `sym_comp_unsym`, `sym_eq_one_iff`, `sym_eq_zero_iff`, `sym_inj`, `sym_injective`, `sym_inv`, `sym_mul_self`, `sym_mul_sym`, `sym_ne_one_iff`, `sym_ne_zero_iff`, `sym_neg`, `sym_one`, `sym_smul`, `sym_sub`, `sym_surjective`, `sym_symm`, `sym_unsym`, `sym_zero`, `unsym_add`, `unsym_bijective`, `unsym_comp_sym`, `unsym_eq_one_iff`, `unsym_eq_zero_iff`, `unsym_inj`, `unsym_injective`, `unsym_inv`, `unsym_mul`, `unsym_mul_self`, `unsym_ne_one_iff`, `unsym_ne_zero_iff`, `unsym_neg`, `unsym_one`, `unsym_smul`, `unsym_sub`, `unsym_surjective`, `unsym_sym`, `unsym_symm`, `unsym_zero`	47
Total	71

SymAlg

Definitions

Name	Category	Theorems
`addCommGroup` 📖	CompOp	—
`addCommMonoid` 📖	CompOp	—
`addCommSemigroup` 📖	CompOp	—
`addGroup` 📖	CompOp	—
`addMonoid` 📖	CompOp	—
`instAdd` 📖	CompOp	2 math math: `unsym_add`, `sym_add`
`instCommMagmaOfInvertibleOfNat` 📖	CompOp	1 math math: `instIsCommJordan`
`instInhabited` 📖	CompOp	—
`instInv` 📖	CompOp	2 math math: `unsym_inv`, `sym_inv`
`instInvertibleCoeEquivSym` 📖	CompOp	1 math math: `invOf_sym`
`instModule` 📖	CompOp	—
`instMulOfAddOfInvertibleOfNat` 📖	CompOp	7 math math: `unsym_mul`, `mul_comm`, `invOf_sym`, `sym_mul_self`, `unsym_mul_self`, `sym_mul_sym`, `mul_def`
`instNeg` 📖	CompOp	2 math math: `sym_neg`, `unsym_neg`
`instNonAssocRingOfInvertibleOfNat` 📖	CompOp	—
`instOne` 📖	CompOp	5 math math: `invOf_sym`, `sym_eq_one_iff`, `unsym_eq_one_iff`, `sym_one`, `unsym_one`
`instSMul` 📖	CompOp	2 math math: `unsym_smul`, `sym_smul`
`instSub` 📖	CompOp	2 math math: `sym_sub`, `unsym_sub`
`instUnique` 📖	CompOp	—
`instZero` 📖	CompOp	4 math math: `sym_zero`, `unsym_zero`, `sym_eq_zero_iff`, `unsym_eq_zero_iff`
`nonAssocSemiring` 📖	CompOp	—
`sym` 📖	CompOp	23 math math: `unsym_comp_sym`, `sym_bijective`, `sym_neg`, `sym_zero`, `sym_add`, `sym_sub`, `sym_injective`, `sym_inv`, `sym_unsym`, `invOf_sym`, `sym_eq_one_iff`, `sym_surjective`, `sym_mul_self`, `sym_inj`, `sym_eq_zero_iff`, `sym_comp_unsym`, `sym_smul`, `unsym_symm`, `sym_one`, `unsym_sym`, `sym_symm`, `sym_mul_sym`, `mul_def`
`unsym` 📖	CompOp	22 math math: `unsym_comp_sym`, `unsym_mul`, `unsym_zero`, `unsym_add`, `unsym_inv`, `sym_unsym`, `unsym_smul`, `unsym_injective`, `unsym_bijective`, `unsym_surjective`, `unsym_eq_one_iff`, `unsym_mul_self`, `unsym_sub`, `sym_comp_unsym`, `unsym_symm`, `unsym_sym`, `unsym_neg`, `sym_symm`, `unsym_one`, `mul_def`, `unsym_inj`, `unsym_eq_zero_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsCommJordan` 📖	mathematical	—	`IsCommJordan` `SymAlg` `instCommMagmaOfInvertibleOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `Commute.add_left` `Commute.one_left` `Commute.eq` `Commute.invOf_left` `one_add_one_eq_two` `mul_def` `unsym_sym` `mul_assoc` `mul_add` `Distrib.leftDistribClass` `add_mul` `Distrib.rightDistribClass` `add_assoc` `unsym_mul_self` `sub_eq_zero` `mul_sub` `add_sub_add_right_eq_sub` `add_sub_add_left_eq_sub` `add_comm` `MulZeroClass.mul_zero`
`instIsEmpty` 📖	mathematical	—	`IsEmpty` `SymAlg`	—	`Function.isEmpty`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `SymAlg`	—	`Function.Injective.nontrivial` `sym_injective`
`instSubsingleton` 📖	mathematical	—	`SymAlg`	—	`Function.Injective.subsingleton` `unsym_injective`
`invOf_sym` 📖	mathematical	—	`Invertible.invOf` `SymAlg` `instMulOfAddOfInvertibleOfNat` `AddSemigroup.toAdd` `AddMonoid.toAddSemigroup` `AddMonoidWithOne.toAddMonoid` `AddMonoidWithOne.toOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat` `instOne` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instInvertibleCoeEquivSym`	—	`Nat.instAtLeastTwoHAddOfNat`
`mul_comm` 📖	mathematical	—	`SymAlg` `instMulOfAddOfInvertibleOfNat` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma`	—	`mul_def` `add_comm`
`mul_def` 📖	mathematical	—	`SymAlg` `instMulOfAddOfInvertibleOfNat` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `Invertible.invOf` `unsym`	—	—
`sym_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instAdd`	—	—
`sym_bijective` 📖	mathematical	—	`Function.Bijective` `SymAlg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym`	—	`Equiv.bijective`
`sym_comp_unsym` 📖	mathematical	—	`SymAlg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `unsym`	—	—
`sym_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instOne`	—	`sym_injective`
`sym_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instZero`	—	`sym_injective`
`sym_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym`	—	`sym_injective`
`sym_injective` 📖	mathematical	—	`SymAlg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym`	—	`Equiv.injective`
`sym_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instInv`	—	—
`sym_mul_self` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `instMulOfAddOfInvertibleOfNat` `Distrib.toAdd` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `sym_mul_sym` `two_mul` `invOf_mul_cancel_left`
`sym_mul_sym` 📖	mathematical	—	`SymAlg` `instMulOfAddOfInvertibleOfNat` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `Invertible.invOf`	—	—
`sym_ne_one_iff` 📖	—	—	—	—	`sym_eq_one_iff`
`sym_ne_zero_iff` 📖	—	—	—	—	`sym_eq_zero_iff`
`sym_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instNeg`	—	—
`sym_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instOne`	—	—
`sym_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instSMul`	—	—
`sym_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instSub`	—	—
`sym_surjective` 📖	mathematical	—	`SymAlg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym`	—	`Equiv.surjective`
`sym_symm` 📖	mathematical	—	`Equiv.symm` `SymAlg` `sym` `unsym`	—	—
`sym_unsym` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `unsym`	—	—
`sym_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `sym` `instZero`	—	—
`unsym_add` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instAdd`	—	—
`unsym_bijective` 📖	mathematical	—	`Function.Bijective` `SymAlg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym`	—	`Equiv.bijective`
`unsym_comp_sym` 📖	mathematical	—	`SymAlg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `sym`	—	—
`unsym_eq_one_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instOne`	—	`unsym_injective`
`unsym_eq_zero_iff` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instZero`	—	`unsym_injective`
`unsym_inj` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym`	—	`unsym_injective`
`unsym_injective` 📖	mathematical	—	`SymAlg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym`	—	`Equiv.injective`
`unsym_inv` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instInv`	—	—
`unsym_mul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instMulOfAddOfInvertibleOfNat` `Invertible.invOf`	—	—
`unsym_mul_self` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instMulOfAddOfInvertibleOfNat` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `Nat.instAtLeastTwoHAddOfNat`	—	`Nat.instAtLeastTwoHAddOfNat` `mul_def` `unsym_sym` `two_mul` `invOf_mul_cancel_left`
`unsym_ne_one_iff` 📖	—	—	—	—	`unsym_eq_one_iff`
`unsym_ne_zero_iff` 📖	—	—	—	—	`unsym_eq_zero_iff`
`unsym_neg` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instNeg`	—	—
`unsym_one` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instOne`	—	—
`unsym_smul` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instSMul`	—	—
`unsym_sub` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instSub`	—	—
`unsym_surjective` 📖	mathematical	—	`SymAlg` `DFunLike.coe` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym`	—	`Equiv.surjective`
`unsym_sym` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `sym`	—	—
`unsym_symm` 📖	mathematical	—	`Equiv.symm` `SymAlg` `unsym` `sym`	—	—
`unsym_zero` 📖	mathematical	—	`DFunLike.coe` `Equiv` `SymAlg` `EquivLike.toFunLike` `Equiv.instEquivLike` `unsym` `instZero`	—	—

(root)

Definitions

Name	Category	Theorems
`SymAlg` 📖	CompOp	43 math math: `SymAlg.unsym_comp_sym`, `SymAlg.sym_bijective`, `SymAlg.sym_neg`, `SymAlg.sym_zero`, `SymAlg.unsym_mul`, `SymAlg.unsym_zero`, `SymAlg.unsym_add`, `SymAlg.sym_add`, `SymAlg.unsym_inv`, `SymAlg.sym_sub`, `SymAlg.sym_injective`, `SymAlg.instNontrivial`, `SymAlg.instIsCommJordan`, `SymAlg.sym_inv`, `SymAlg.sym_unsym`, `SymAlg.mul_comm`, `SymAlg.invOf_sym`, `SymAlg.sym_eq_one_iff`, `SymAlg.unsym_smul`, `SymAlg.unsym_injective`, `SymAlg.sym_surjective`, `SymAlg.sym_mul_self`, `SymAlg.unsym_bijective`, `SymAlg.unsym_surjective`, `SymAlg.unsym_eq_one_iff`, `SymAlg.sym_inj`, `SymAlg.instSubsingleton`, `SymAlg.unsym_mul_self`, `SymAlg.sym_eq_zero_iff`, `SymAlg.unsym_sub`, `SymAlg.sym_comp_unsym`, `SymAlg.sym_smul`, `SymAlg.unsym_symm`, `SymAlg.instIsEmpty`, `SymAlg.sym_one`, `SymAlg.unsym_sym`, `SymAlg.unsym_neg`, `SymAlg.sym_symm`, `SymAlg.sym_mul_sym`, `SymAlg.unsym_one`, `SymAlg.mul_def`, `SymAlg.unsym_inj`, `SymAlg.unsym_eq_zero_iff`
`«term_ˢʸᵐ»` 📖	CompOp	—

---

← Back to Index