Inversion

📁 Source: Mathlib/LinearAlgebra/CliffordAlgebra/Inversion.lean

Statistics

Metric	Count
Definitions invertibleOfInvertibleι, invertibleιOfInvertible	2
Theorems invOf_ι, invOf_ι_mul_ι_mul_ι, isUnit_of_isUnit_ι, isUnit_ι_iff, isUnit_ι_of_isUnit, ι_mul_ι_mul_invOf_ι	6
Total	8

CliffordAlgebra

Definitions

Name	Category	Theorems
invertibleOfInvertibleι 📖	CompOp	—
invertibleιOfInvertible 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
invOf_ι 📖	mathematical	—	Invertible.invOf CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instModule LinearMap.instFunLike ι SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRing.toRing QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Invertible.congr
invOf_ι_mul_ι_mul_ι 📖	mathematical	—	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Invertible.invOf AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instModule LinearMap.instFunLike ι SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRing.toRing QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule QuadraticMap.polar Ring.toAddCommGroup	—	invOf_ι map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass smul_mul_assoc IsScalarTower.right ι_mul_ι_mul_ι smul_sub smul_smul invOf_mul_self one_smul
isUnit_of_isUnit_ι 📖	mathematical	IsUnit CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instModule LinearMap.instFunLike ι	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	—	Nat.instAtLeastTwoHAddOfNat IsUnit.nonempty_invertible isUnit_of_invertible
isUnit_ι_iff 📖	mathematical	—	IsUnit CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instModule LinearMap.instFunLike ι QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	Nat.instAtLeastTwoHAddOfNat isUnit_of_isUnit_ι isUnit_ι_of_isUnit
isUnit_ι_of_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instFunLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule	IsUnit CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instModule LinearMap.instFunLike ι	—	IsUnit.nonempty_invertible isUnit_of_invertible
ι_mul_ι_mul_invOf_ι 📖	mathematical	—	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid instModule LinearMap.instFunLike ι Invertible.invOf AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRing.toRing QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule QuadraticMap.polar Ring.toAddCommGroup	—	invOf_ι map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass mul_smul_comm Algebra.to_smulCommClass ι_mul_ι_mul_ι smul_sub smul_smul invOf_mul_self one_smul

---

← Back to Index