SpinGroup

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

Statistics

Metric	Count
Definitions lipschitzGroup, pinGroup, instGroupSubtypeCliffordAlgebraMemSubmonoid, instInhabitedSubtypeCliffordAlgebraMemSubmonoid, instStarMulSubtypeCliffordAlgebraMemSubmonoid, instStarSubtypeCliffordAlgebraMemSubmonoid, toUnits, spinGroup, instGroupSubtypeCliffordAlgebraMemSubmonoid, instInhabitedSubtypeCliffordAlgebraMemSubmonoid, instStarMulSubtypeCliffordAlgebraMemSubmonoid, instStarSubtypeCliffordAlgebraMemSubmonoid, toUnits	13
Theorems coe_mem_iff_mem, conjAct_smul_range_ι, conjAct_smul_ι_mem_range_ι, involute_act_ι_mem_range_ι, coe_mul_star_self, coe_star, coe_star_mul_self, conjAct_smul_range_ι, conjAct_smul_ι_mem_range_ι, involute_act_ι_mem_range_ι, mem_iff, mem_lipschitzGroup, mem_unitary, mul_star_self, mul_star_self_of_mem, star_eq_inv, star_eq_inv', star_mem, star_mem_iff, star_mul_self, star_mul_self_of_mem, toUnits_injective, units_mem_iff, units_mem_lipschitzGroup, val_inv_toUnits_apply, val_toUnits_apply, coe_mul_star_self, coe_star, coe_star_mul_self, conjAct_smul_range_ι, conjAct_smul_ι_mem_range_ι, involute_act_ι_mem_range_ι, involute_eq, mem_even, mem_iff, mem_pin, mul_star_self, mul_star_self_of_mem, star_eq_inv, star_eq_inv', star_mem, star_mem_iff, star_mul_self, star_mul_self_of_mem, toUnits_injective, units_involute_act_eq_conjAct, units_mem_lipschitzGroup, val_inv_toUnits_apply, val_toUnits_apply	49
Total	62

(root)

Definitions

Name	Category	Theorems
lipschitzGroup 📖	CompOp	6 math math: spinGroup.units_mem_lipschitzGroup, pinGroup.units_mem_iff, pinGroup.units_mem_lipschitzGroup, pinGroup.mem_lipschitzGroup, pinGroup.mem_iff, lipschitzGroup.coe_mem_iff_mem
pinGroup 📖	CompOp	15 math math: pinGroup.coe_star_mul_self, pinGroup.val_inv_toUnits_apply, pinGroup.star_mul_self, spinGroup.mem_iff, pinGroup.val_toUnits_apply, pinGroup.star_eq_inv', pinGroup.units_mem_iff, pinGroup.toUnits_injective, pinGroup.mul_star_self, pinGroup.star_mem_iff, spinGroup.mem_pin, pinGroup.mem_iff, pinGroup.star_eq_inv, pinGroup.coe_star, pinGroup.coe_mul_star_self
spinGroup 📖	CompOp	12 math math: spinGroup.star_eq_inv, spinGroup.coe_star_mul_self, spinGroup.star_eq_inv', spinGroup.mem_iff, spinGroup.coe_mul_star_self, spinGroup.val_inv_toUnits_apply, spinGroup.mul_star_self, spinGroup.coe_star, spinGroup.toUnits_injective, spinGroup.star_mul_self, spinGroup.val_toUnits_apply, spinGroup.star_mem_iff

lipschitzGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mem_iff_mem 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike Submonoid.map Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Units.instGroup MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike MonoidHom.instMonoidHomClass Units.coeHom Subgroup.toSubmonoid lipschitzGroup Units.val Subgroup Subgroup.instSetLike	—	MonoidHom.instMonoidHomClass
conjAct_smul_range_ι 📖	mathematical	Units CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike lipschitzGroup	ConjAct Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Units.instDivInvMonoid Submodule.pointwiseDistribMulAction MulSemiringAction.toDistribMulAction ConjAct.unitsMulSemiringAction ConjAct.unitsSMulCommClass' AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule IsScalarTower.right RingQuot.instSemiring TensorAlgebra AddCommGroup.toAddCommMonoid instSemiringTensorAlgebra CliffordAlgebra.Rel DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct LinearMap.range RingHom.id RingHomSurjective.ids CliffordAlgebra.ι	—	Nat.instAtLeastTwoHAddOfNat ConjAct.unitsSMulCommClass' IsScalarTower.to_smulCommClass' IsScalarTower.right RingHomSurjective.ids Submodule.map_le_iff_le_comap conjAct_smul_ι_mem_range_ι le_antisymm smul_mono_right Submodule.instCovariantClassHSMulLe InvMemClass.inv_mem SubgroupClass.toInvMemClass Subgroup.instSubgroupClass Eq.trans_le map_inv MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass smul_inv_smul
conjAct_smul_ι_mem_range_ι 📖	mathematical	Units CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike lipschitzGroup	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra Submodule.setLike LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids CliffordAlgebra.ι ConjAct ConjAct.unitsScalar DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Units.instDivInvMonoid ConjAct.instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct LinearMap LinearMap.instFunLike	—	Nat.instAtLeastTwoHAddOfNat RingHomSurjective.ids ConjAct.units_smul_def ConjAct.ofConjAct_toConjAct Subgroup.closure_induction'' invOf_units Invertible.congr CliffordAlgebra.ι_mul_ι_mul_invOf_ι inv_inv CliffordAlgebra.invOf_ι_mul_ι_mul_ι inv_one one_mul mul_one mul_inv_rev mul_assoc
involute_act_ι_mem_range_ι 📖	mathematical	Units CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra Subgroup Units.instGroup SetLike.instMembership Subgroup.instSetLike lipschitzGroup	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra Submodule.setLike LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids CliffordAlgebra.ι Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe AlgHom AlgHom.funLike CliffordAlgebra.involute Units.val LinearMap LinearMap.instFunLike Units.instInv	—	Nat.instAtLeastTwoHAddOfNat Subgroup.closure_induction'' RingHomSurjective.ids invOf_units Invertible.congr CliffordAlgebra.involute_ι neg_mul CliffordAlgebra.ι_mul_ι_mul_invOf_ι DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass inv_inv MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass map_invOf invOf_neg CliffordAlgebra.invOf_ι_mul_ι_mul_ι inv_one map_one MonoidHomClass.toOneHomClass one_mul mul_one mul_inv_rev map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass mul_assoc

pinGroup

Definitions

Name	Category	Theorems
instGroupSubtypeCliffordAlgebraMemSubmonoid 📖	CompOp	3 math math: val_inv_toUnits_apply, star_eq_inv', star_eq_inv
instInhabitedSubtypeCliffordAlgebraMemSubmonoid 📖	CompOp	—
instStarMulSubtypeCliffordAlgebraMemSubmonoid 📖	CompOp	—
instStarSubtypeCliffordAlgebraMemSubmonoid 📖	CompOp	6 math math: star_mul_self, star_eq_inv', mul_star_self, star_eq_inv, coe_star, coe_mul_star_self
toUnits 📖	CompOp	3 math math: val_inv_toUnits_apply, val_toUnits_apply, toUnits_injective

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mul_star_self 📖	mathematical	—	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SetLike.instMembership Submonoid.instSetLike pinGroup Star.star instStarSubtypeCliffordAlgebraMemSubmonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	mul_star_self_of_mem Subtype.prop
coe_star 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Star.star instStarSubtypeCliffordAlgebraMemSubmonoid InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid CliffordAlgebra.instStarRing	—	—
coe_star_mul_self 📖	mathematical	—	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CliffordAlgebra.instStarRing Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SetLike.instMembership Submonoid.instSetLike pinGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	star_mul_self_of_mem Subtype.prop
conjAct_smul_range_ι 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	ConjAct Units Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Units.instDivInvMonoid Submodule.pointwiseDistribMulAction MulSemiringAction.toDistribMulAction ConjAct.unitsMulSemiringAction ConjAct.unitsSMulCommClass' AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule IsScalarTower.right RingQuot.instSemiring TensorAlgebra AddCommGroup.toAddCommMonoid instSemiringTensorAlgebra CliffordAlgebra.Rel DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct LinearMap.range RingHom.id RingHomSurjective.ids CliffordAlgebra.ι	—	Nat.instAtLeastTwoHAddOfNat lipschitzGroup.conjAct_smul_range_ι units_mem_lipschitzGroup
conjAct_smul_ι_mem_range_ι 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra Submodule.setLike LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id RingHomSurjective.ids CliffordAlgebra.ι ConjAct Units ConjAct.unitsScalar DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Units.instDivInvMonoid ConjAct.instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct LinearMap LinearMap.instFunLike	—	Nat.instAtLeastTwoHAddOfNat lipschitzGroup.conjAct_smul_ι_mem_range_ι units_mem_lipschitzGroup
involute_act_ι_mem_range_ι 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra Submodule.setLike LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id RingHomSurjective.ids CliffordAlgebra.ι Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe AlgHom AlgHom.funLike CliffordAlgebra.involute LinearMap LinearMap.instFunLike Units Units.instInv	—	Nat.instAtLeastTwoHAddOfNat lipschitzGroup.involute_act_ι_mem_range_ι units_mem_lipschitzGroup
mem_iff 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Submonoid.map Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Units.instGroup MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike MonoidHom.instMonoidHomClass Units.coeHom Subgroup.toSubmonoid lipschitzGroup unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CliffordAlgebra.instStarRing	—	—
mem_lipschitzGroup 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup	Submonoid.map Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Units.instGroup MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike MonoidHom.instMonoidHomClass Units.coeHom Subgroup.toSubmonoid lipschitzGroup	—	—
mem_unitary 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup	Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CliffordAlgebra.instStarRing	—	—
mul_star_self 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Submonoid.mul Star.star instStarSubtypeCliffordAlgebraMemSubmonoid Submonoid.one	—	coe_mul_star_self
mul_star_self_of_mem 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CliffordAlgebra.instStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
star_eq_inv 📖	mathematical	—	Star.star CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup instStarSubtypeCliffordAlgebraMemSubmonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroupSubtypeCliffordAlgebraMemSubmonoid	—	—
star_eq_inv' 📖	mathematical	—	Star.star CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup instStarSubtypeCliffordAlgebraMemSubmonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroupSubtypeCliffordAlgebraMemSubmonoid	—	—
star_mem 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid CliffordAlgebra.instStarRing	—	MonoidHom.instMonoidHomClass mem_iff inv_mul_cancel_left mul_one SubgroupClass.toInvMemClass Subgroup.instSubgroupClass Unitary.star_mem
star_mem_iff 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid CliffordAlgebra.instStarRing	—	star_star star_mem
star_mul_self 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Submonoid.mul Star.star instStarSubtypeCliffordAlgebraMemSubmonoid Submonoid.one	—	coe_star_mul_self
star_mul_self_of_mem 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CliffordAlgebra.instStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
toUnits_injective 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Submonoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike toUnits	—	Units.ext_iff
units_mem_iff 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units Subgroup Units.instGroup Subgroup.instSetLike lipschitzGroup Monoid.toMulOneClass unitary StarRing.toStarMul NonUnitalSemiring.toNonUnitalNonAssocSemiring Semiring.toNonUnitalSemiring CliffordAlgebra.instStarRing	—	MonoidHom.instMonoidHomClass mem_iff lipschitzGroup.coe_mem_iff_mem
units_mem_lipschitzGroup 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike pinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Units Subgroup Units.instGroup Subgroup.instSetLike lipschitzGroup	—	units_mem_iff
val_inv_toUnits_apply 📖	mathematical	—	Units.val CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra Units Units.instInv DFunLike.coe MonoidHom Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike pinGroup MulOneClass.toMulOne Submonoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike toUnits InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroupSubtypeCliffordAlgebraMemSubmonoid	—	—
val_toUnits_apply 📖	mathematical	—	Units.val CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra DFunLike.coe MonoidHom Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike pinGroup Units MulOneClass.toMulOne Submonoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike toUnits	—	—

spinGroup

Definitions

Name	Category	Theorems
instGroupSubtypeCliffordAlgebraMemSubmonoid 📖	CompOp	3 math math: star_eq_inv, star_eq_inv', val_inv_toUnits_apply
instInhabitedSubtypeCliffordAlgebraMemSubmonoid 📖	CompOp	—
instStarMulSubtypeCliffordAlgebraMemSubmonoid 📖	CompOp	—
instStarSubtypeCliffordAlgebraMemSubmonoid 📖	CompOp	6 math math: star_eq_inv, star_eq_inv', coe_mul_star_self, mul_star_self, coe_star, star_mul_self
toUnits 📖	CompOp	3 math math: val_inv_toUnits_apply, toUnits_injective, val_toUnits_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mul_star_self 📖	mathematical	—	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SetLike.instMembership Submonoid.instSetLike spinGroup Star.star instStarSubtypeCliffordAlgebraMemSubmonoid AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	mul_star_self_of_mem Subtype.prop
coe_star 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Star.star instStarSubtypeCliffordAlgebraMemSubmonoid InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid CliffordAlgebra.instStarRing	—	—
coe_star_mul_self 📖	mathematical	—	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CliffordAlgebra.instStarRing Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring SetLike.instMembership Submonoid.instSetLike spinGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	star_mul_self_of_mem Subtype.prop
conjAct_smul_range_ι 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	ConjAct Units Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne Submodule.instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul DivInvMonoid.toMonoid ConjAct.instDivInvMonoid Units.instDivInvMonoid Submodule.pointwiseDistribMulAction MulSemiringAction.toDistribMulAction ConjAct.unitsMulSemiringAction ConjAct.unitsSMulCommClass' AddCommMonoid.toAddMonoid Module.toDistribMulAction IsScalarTower.to_smulCommClass' NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule IsScalarTower.right RingQuot.instSemiring TensorAlgebra AddCommGroup.toAddCommMonoid instSemiringTensorAlgebra CliffordAlgebra.Rel DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct LinearMap.range RingHom.id RingHomSurjective.ids CliffordAlgebra.ι	—	Nat.instAtLeastTwoHAddOfNat lipschitzGroup.conjAct_smul_range_ι units_mem_lipschitzGroup
conjAct_smul_ι_mem_range_ι 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra Submodule.setLike LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id RingHomSurjective.ids CliffordAlgebra.ι ConjAct Units ConjAct.unitsScalar DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Units.instDivInvMonoid ConjAct.instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct LinearMap LinearMap.instFunLike	—	Nat.instAtLeastTwoHAddOfNat lipschitzGroup.conjAct_smul_ι_mem_range_ι units_mem_lipschitzGroup
involute_act_ι_mem_range_ι 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra Submodule.setLike LinearMap.range AddCommGroup.toAddCommMonoid RingHom.id RingHomSurjective.ids CliffordAlgebra.ι Distrib.toMul NonUnitalNonAssocSemiring.toDistrib DFunLike.coe AlgHom AlgHom.funLike CliffordAlgebra.involute LinearMap LinearMap.instFunLike Units Units.instInv	—	Nat.instAtLeastTwoHAddOfNat lipschitzGroup.involute_act_ι_mem_range_ι units_mem_lipschitzGroup
involute_eq 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup	DFunLike.coe AlgHom CommRing.toCommSemiring instAlgebraCliffordAlgebra AlgHom.funLike CliffordAlgebra.involute	—	CliffordAlgebra.involute_eq_of_mem_even mem_even
mem_even 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup	Subalgebra CommRing.toCommSemiring instAlgebraCliffordAlgebra Subalgebra.instSetLike CliffordAlgebra.even	—	—
mem_iff 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup pinGroup Subalgebra CommRing.toCommSemiring instAlgebraCliffordAlgebra Subalgebra.instSetLike CliffordAlgebra.even	—	—
mem_pin 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup	pinGroup	—	—
mul_star_self 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Submonoid.mul Star.star instStarSubtypeCliffordAlgebraMemSubmonoid Submonoid.one	—	coe_mul_star_self
mul_star_self_of_mem 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CliffordAlgebra.instStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
star_eq_inv 📖	mathematical	—	Star.star CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup instStarSubtypeCliffordAlgebraMemSubmonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroupSubtypeCliffordAlgebraMemSubmonoid	—	—
star_eq_inv' 📖	mathematical	—	Star.star CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup instStarSubtypeCliffordAlgebraMemSubmonoid InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroupSubtypeCliffordAlgebraMemSubmonoid	—	—
star_mem 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup	Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid CliffordAlgebra.instStarRing	—	mem_iff pinGroup.star_mem
star_mem_iff 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing StarRing.toStarAddMonoid CliffordAlgebra.instStarRing	—	star_star star_mem
star_mul_self 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Submonoid.mul Star.star instStarSubtypeCliffordAlgebraMemSubmonoid Submonoid.one	—	coe_star_mul_self
star_mul_self_of_mem 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Star.star InvolutiveStar.toStar StarAddMonoid.toInvolutiveStar AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid StarRing.toStarAddMonoid CliffordAlgebra.instStarRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
toUnits_injective 📖	mathematical	—	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe MonoidHom MulOneClass.toMulOne Submonoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike toUnits	—	Units.ext_iff
units_involute_act_eq_conjAct 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe AlgHom CommRing.toCommSemiring instAlgebraCliffordAlgebra AlgHom.funLike CliffordAlgebra.involute LinearMap CommSemiring.toSemiring RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike CliffordAlgebra.ι Units Units.instInv ConjAct ConjAct.unitsScalar MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Units.instDivInvMonoid ConjAct.instDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike ConjAct.toConjAct	—	involute_eq ConjAct.units_smul_def ConjAct.ofConjAct_toConjAct
units_mem_lipschitzGroup 📖	mathematical	CliffordAlgebra Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra SetLike.instMembership Submonoid.instSetLike spinGroup Units.val MonoidWithZero.toMonoid Semiring.toMonoidWithZero	Units Subgroup Units.instGroup Subgroup.instSetLike lipschitzGroup	—	pinGroup.units_mem_lipschitzGroup mem_pin
val_inv_toUnits_apply 📖	mathematical	—	Units.val CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra Units Units.instInv DFunLike.coe MonoidHom Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike spinGroup MulOneClass.toMulOne Submonoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike toUnits InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid instGroupSubtypeCliffordAlgebraMemSubmonoid	—	—
val_toUnits_apply 📖	mathematical	—	Units.val CliffordAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra DFunLike.coe MonoidHom Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike spinGroup Units MulOneClass.toMulOne Submonoid.toMulOneClass Units.instMulOneClass MonoidHom.instFunLike toUnits	—	—

---

← Back to Index