Basic

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

Statistics

Metric	Count
Definitions CliffordAlgebra, equivOfIsometry, instAlgebra', map, ι, toClifford, instAlgebraCliffordAlgebra, instInhabitedCliffordAlgebra, instRingCliffordAlgebra	9
Theorems adjoin_range_ι, comp_ι_sq_scalar, equivOfIsometry_apply, equivOfIsometry_refl, equivOfIsometry_symm, equivOfIsometry_trans, forall_mul_self_eq_iff, hom_ext, hom_ext_iff, induction, instIsScalarTower, instSMulCommClass, leftInverse_map_of_leftInverse, lift_comp_ι, lift_symm_apply, lift_unique, lift_ι_apply, map_apply_ι, map_comp_map, map_comp_ι, map_id, map_surjective, mul_add_swap_eq_polar_of_forall_mul_self_eq, mul_ι_mul_ι_of_isOrtho, range_lift, ι_comp_lift, ι_mul_ι_add_swap, ι_mul_ι_add_swap_of_isOrtho, ι_mul_ι_comm, ι_mul_ι_comm_of_isOrtho, ι_mul_ι_mul_of_isOrtho, ι_mul_ι_mul_ι, ι_range_map_lift, ι_range_map_map, ι_sq_scalar, toClifford_ι	36
Total	45

CliffordAlgebra

Definitions

Name	Category	Theorems
equivOfIsometry 📖	CompOp	4 math math: equivOfIsometry_trans, equivOfIsometry_refl, equivOfIsometry_symm, equivOfIsometry_apply
instAlgebra' 📖	CompOp	3 math math: instSMulCommClass, ofBaseChangeAux_ι, instIsScalarTower
map 📖	CompOp	13 math math: ι_range_map_map, map_id, commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_right, map_mul_map_of_isOrtho_of_mem_evenOdd, map_apply_ι, QuadraticModuleCat.cliffordAlgebra_map, map_comp_ι, commute_map_mul_map_of_isOrtho_of_mem_evenOdd_zero_left, map_surjective, equivOfIsometry_apply, map_comp_map, map_mul_map_eq_neg_of_isOrtho_of_mem_evenOdd_one, leftInverse_map_of_leftInverse
ι 📖	CompOp	86 math math: ι_range_map_map, CliffordAlgebraQuaternion.j_quaternionBasis, mul_ι_mul_ι_of_isOrtho, foldl_prod_map_ι, ι_mul_ι_mul_invOf_ι, involute_prod_map_ι, lift_ι_apply, CliffordAlgebraDualNumber.equiv_symm_eps, contractRight_mul_ι, toProd_ι_tmul_one, ι_mul_ι_comm, ι_range_map_lift, ι_sq_scalar, EquivEven.ι_eq_v_add_smul_e0, ι_comp_lift, lift_unique, foldr_prod_map_ι, changeFormAux_apply_apply, CliffordAlgebraQuaternion.k_quaternionBasis, changeForm_ι_mul, CliffordAlgebraQuaternion.i_quaternionBasis, lipschitzGroup.conjAct_smul_ι_mem_range_ι, spinGroup.units_involute_act_eq_conjAct, spinGroup.conjAct_smul_ι_mem_range_ι, ι_mul_ι_mul_ι, spinGroup.involute_act_ι_mem_range_ι, adjoin_range_ι, spinGroup.conjAct_smul_range_ι, range_ι_le_evenOdd_one, CliffordAlgebraComplex.ofComplex_I, TensorAlgebra.toClifford_ι, hom_ext_iff, invOf_ι_mul_ι_mul_ι, map_apply_ι, ι_mul_ι_add_swap, contractLeft_ι_mul, comp_ι_sq_scalar, ι_range_map_reverse, ι_range_map_involute, pinGroup.conjAct_smul_ι_mem_range_ι, GradedAlgebra.ι_apply, isUnit_ι_iff, changeForm_ι_mul_ι, ι_range_comap_involute, reverse_prod_map_ι, ofBaseChange_tmul_ι, ι_mul_ι_mem_evenOdd_zero, ofBaseChangeAux_ι, foldr_ι, lift_symm_apply, foldl_ι, CliffordAlgebraQuaternion.ofQuaternion_mk, pinGroup.conjAct_smul_range_ι, map_comp_ι, CliffordAlgebraComplex.toComplex_ι, changeForm_ι, ι_mul_ι_add_swap_of_isOrtho, contractLeft_ι, invOf_ι, star_ι, involute_ι, CliffordAlgebraRing.ι_eq_zero, toEven_ι, CliffordAlgebraDualNumber.equiv_ι, foldr'Aux_apply_apply, reverseOp_ι, ι_mul_ι_comm_of_isOrtho, iSup_ι_range_eq_top, toProd_one_tmul_ι, pinGroup.involute_act_ι_mem_range_ι, CliffordAlgebraDualNumber.ι_mul_ι, isUnit_ι_of_isUnit, lift_comp_ι, ofEven_ι, toBaseChange_ι, ι_mem_evenOdd_one, ofProd_ι_mk, lipschitzGroup.involute_act_ι_mem_range_ι, contractRight_ι, ι_range_comap_reverse, CliffordAlgebraQuaternion.toQuaternion_ι, contractLeftAux_apply_apply, contractLeftAux_contractLeftAux, lipschitzGroup.conjAct_smul_range_ι, reverse_ι, ι_mul_ι_mul_of_isOrtho

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoin_range_ι 📖	mathematical	—	Algebra.adjoin CliffordAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra Set.range DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	top_unique induction algebraMap_mem AddSubmonoidWithOneClass.toOneMemClass SubsemiringClass.addSubmonoidWithOneClass Subalgebra.instSubsemiringClass Subalgebra.instSMulMemClass Algebra.subset_adjoin Set.mem_range_self MulMemClass.mul_mem SubmonoidClass.toMulMemClass SubsemiringClass.toSubmonoidClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass SubsemiringClass.toAddSubmonoidClass
comp_ι_sq_scalar 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom CliffordAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra AlgHom.funLike LinearMap CommSemiring.toSemiring RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike Semiring.toModule	—	map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass ι_sq_scalar AlgHom.commutes
equivOfIsometry_apply 📖	mathematical	—	DFunLike.coe AlgEquiv CliffordAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra AlgEquiv.instFunLike equivOfIsometry AlgHom AlgHom.funLike map QuadraticMap.IsometryEquiv.toIsometry AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	—	—
equivOfIsometry_refl 📖	mathematical	—	equivOfIsometry QuadraticMap.IsometryEquiv.refl CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule AlgEquiv.refl CliffordAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra	—	AlgEquiv.ext AlgHom.congr_fun map_id
equivOfIsometry_symm 📖	mathematical	—	AlgEquiv.symm CliffordAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra equivOfIsometry QuadraticMap.IsometryEquiv.symm AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	—	—
equivOfIsometry_trans 📖	mathematical	—	AlgEquiv.trans CliffordAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra equivOfIsometry QuadraticMap.IsometryEquiv.trans AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	—	AlgEquiv.ext AlgHom.congr_fun map_comp_map
forall_mul_self_eq_iff 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instOfNatAtLeastTwo AddMonoidWithOne.toNatCast AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Nat.instAtLeastTwoHAddOfNat	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction SMulCommClass.symm SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul LinearMap.instAdd LinearMap.comp RingHomCompTriple.ids LinearMap.compl₂ LinearMap.mul Algebra.to_smulCommClass IsScalarTower.right LinearMap.flip LinearMap.compr₂ Ring.toAddCommGroup CommRing.toRing CommRing.toCommMonoid IsScalarTower.left Algebra.id QuadraticMap.polarBilin Algebra.linearMap	—	Nat.instAtLeastTwoHAddOfNat smulCommClass_self SMulCommClass.symm RingHomCompTriple.ids Algebra.to_smulCommClass IsScalarTower.right IsScalarTower.left mul_add_swap_eq_polar_of_forall_mul_self_eq IsUnit.mul_left_cancel two_mul QuadraticMap.polar_self two_smul map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
hom_ext 📖	—	LinearMap.comp CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap ι	—	—	RingHomCompTriple.ids Equiv.injective lift_symm_apply
hom_ext_iff 📖	mathematical	—	LinearMap.comp CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap ι	—	RingHomCompTriple.ids hom_ext
induction 📖	—	DFunLike.coe RingHom CliffordAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra LinearMap RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd	—	—	RingHom.map_one RingHom.map_zero ι_sq_scalar hom_ext LinearMap.ext RingHomCompTriple.ids lift_ι_apply LinearMap.codRestrict_apply AlgHom.id_apply Subtype.prop
instIsScalarTower 📖	mathematical	—	IsScalarTower CliffordAlgebra Algebra.toSMul Ring.toSemiring instRingCliffordAlgebra instAlgebra'	—	RingQuot.instIsScalarTower instIsScalarTowerTensorAlgebra
instSMulCommClass 📖	mathematical	—	SMulCommClass CliffordAlgebra Algebra.toSMul Ring.toSemiring instRingCliffordAlgebra instAlgebra'	—	RingQuot.instSMulCommClass instSMulCommClassTensorAlgebra
leftInverse_map_of_leftInverse 📖	mathematical	DFunLike.coe QuadraticMap.Isometry CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticMap.Isometry.instFunLike	CliffordAlgebra AlgHom Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra AlgHom.funLike map	—	DFunLike.ext AlgHom.comp_apply map_comp_map map_id AlgHom.coe_id
lift_comp_ι 📖	mathematical	—	DFunLike.coe Equiv LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom CliffordAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra EquivLike.toFunLike Equiv.instEquivLike lift LinearMap.comp RingHomCompTriple.ids AlgHom.toLinearMap ι comp_ι_sq_scalar	—	Equiv.apply_symm_apply
lift_symm_apply 📖	mathematical	—	DFunLike.coe Equiv AlgHom CliffordAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift LinearMap.comp AlgHom.toLinearMap ι	—	—
lift_unique 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike Semiring.toModule	LinearMap.comp CliffordAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra RingHomCompTriple.ids AlgHom.toLinearMap ι Equiv AlgHom EquivLike.toFunLike Equiv.instEquivLike lift	—	RingHomCompTriple.ids lift_symm_apply Equiv.symm_apply_eq
lift_ι_apply 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike Semiring.toModule	AlgHom CliffordAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra AlgHom.funLike Equiv EquivLike.toFunLike Equiv.instEquivLike lift NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ι	—	RingHomCompTriple.ids LinearMap.ext_iff ι_comp_lift
map_apply_ι 📖	mathematical	—	DFunLike.coe AlgHom CliffordAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra AlgHom.funLike map LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι QuadraticMap.Isometry NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule QuadraticMap.Isometry.instFunLike	—	lift_ι_apply
map_comp_map 📖	mathematical	—	AlgHom.comp CliffordAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra map QuadraticMap.Isometry.comp AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	—	hom_ext LinearMap.ext RingHomCompTriple.ids map_apply_ι QuadraticMap.Isometry.comp_apply
map_comp_ι 📖	mathematical	—	LinearMap.comp CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap map ι NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing QuadraticMap.Isometry.toLinearMap Semiring.toModule	—	ι_comp_lift
map_id 📖	mathematical	—	map QuadraticMap.Isometry.id CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule AlgHom.id CliffordAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra	—	hom_ext LinearMap.ext RingHomCompTriple.ids map_apply_ι
map_surjective 📖	mathematical	DFunLike.coe QuadraticMap.Isometry CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule QuadraticMap.Isometry.instFunLike	CliffordAlgebra AlgHom Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra AlgHom.funLike map	—	induction AlgHom.commutes map_apply_ι map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass
mul_add_swap_eq_polar_of_forall_mul_self_eq 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule Ring.toSemiring LinearMap.instFunLike RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	Distrib.toAdd QuadraticMap.polar Ring.toAddCommGroup CommRing.toRing	—	LinearMap.map_add mul_add Distrib.leftDistribClass add_mul Distrib.rightDistribClass Mathlib.Tactic.Abel.subst_into_addg Mathlib.Tactic.Abel.term_atomg Mathlib.Tactic.Abel.term_add_constg zero_add Mathlib.Tactic.Abel.unfold_sub Mathlib.Tactic.Abel.const_add_termg add_zero Mathlib.Tactic.Abel.subst_into_negg Mathlib.Tactic.Abel.term_neg neg_zero Mathlib.Tactic.Abel.term_add_termg Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.isInt_neg Mathlib.Tactic.Abel.zero_termg map_sub RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
mul_ι_mul_ι_of_isOrtho 📖	mathematical	QuadraticMap.IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra DFunLike.coe LinearMap RingHom.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	mul_assoc ι_mul_ι_comm_of_isOrtho mul_neg
range_lift 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike Semiring.toModule	AlgHom.range CliffordAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra Equiv AlgHom EquivLike.toFunLike Equiv.instEquivLike lift Algebra.adjoin Set.range	—	AlgHom.map_adjoin lift_ι_apply
ι_comp_lift 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike Semiring.toModule	LinearMap.comp CliffordAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra RingHomCompTriple.ids AlgHom.toLinearMap Equiv AlgHom EquivLike.toFunLike Equiv.instEquivLike lift ι	—	RingHomCompTriple.ids Equiv.symm_apply_apply
ι_mul_ι_add_swap 📖	mathematical	—	CliffordAlgebra Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Distrib.toMul DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι RingHom RingHom.instFunLike algebraMap QuadraticMap.polar Ring.toAddCommGroup CommRing.toRing QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	mul_add_swap_eq_polar_of_forall_mul_self_eq ι_sq_scalar
ι_mul_ι_add_swap_of_isOrtho 📖	mathematical	QuadraticMap.IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	CliffordAlgebra Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra Distrib.toMul DFunLike.coe LinearMap RingHom.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	ι_mul_ι_add_swap QuadraticMap.IsOrtho.polar_eq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ι_mul_ι_comm 📖	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 Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne RingHom RingHom.instFunLike algebraMap QuadraticMap.polar Ring.toAddCommGroup CommRing.toRing QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	eq_sub_of_add_eq ι_mul_ι_add_swap
ι_mul_ι_comm_of_isOrtho 📖	mathematical	QuadraticMap.IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra DFunLike.coe LinearMap RingHom.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	eq_neg_of_add_eq_zero_left ι_mul_ι_add_swap_of_isOrtho
ι_mul_ι_mul_of_isOrtho 📖	mathematical	QuadraticMap.IsOrtho CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule	CliffordAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra DFunLike.coe LinearMap RingHom.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup	—	mul_assoc ι_mul_ι_comm_of_isOrtho neg_mul
ι_mul_ι_mul_ι 📖	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 Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra 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 QuadraticMap.polar Ring.toAddCommGroup CommRing.toRing QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	ι_mul_ι_comm sub_mul mul_assoc ι_sq_scalar Algebra.smul_def Algebra.commutes map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass
ι_range_map_lift 📖	mathematical	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule LinearMap.instFunLike RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike Semiring.toModule	Submodule.map CliffordAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebraCliffordAlgebra RingHomSurjective.ids AlgHom.toLinearMap Equiv AlgHom EquivLike.toFunLike Equiv.instEquivLike lift LinearMap.range NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ι	—	RingHomSurjective.ids RingHomCompTriple.ids LinearMap.range_comp ι_comp_lift
ι_range_map_map 📖	mathematical	—	Submodule.map CliffordAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomSurjective.ids AlgHom.toLinearMap map LinearMap.range AddCommGroup.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ι QuadraticMap.Isometry.toLinearMap Semiring.toModule	—	RingHomSurjective.ids ι_range_map_lift LinearMap.range_comp
ι_sq_scalar 📖	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 Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι RingHom RingHom.instFunLike algebraMap QuadraticForm QuadraticMap.instFunLike NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule	—	ι.eq_1 LinearMap.comp_apply AlgHom.toLinearMap_apply IsScalarTower.left map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass RingQuot.mkAlgHom_rel AlgHom.commutes

TensorAlgebra

Definitions

Name	Category	Theorems
toClifford 📖	CompOp	1 math math: toClifford_ι

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toClifford_ι 📖	mathematical	—	DFunLike.coe AlgHom TensorAlgebra CommRing.toCommSemiring AddCommGroup.toAddCommMonoid CliffordAlgebra instSemiringTensorAlgebra Ring.toSemiring instRingCliffordAlgebra instAlgebra Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction instAlgebraCliffordAlgebra AlgHom.funLike toClifford LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike ι NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing CliffordAlgebra.ι	—	IsScalarTower.left lift_ι_apply

(root)

Definitions

Name	Category	Theorems
CliffordAlgebra 📖	CompOp	250 math math: CliffordAlgebra.unop_reverseOp, CliffordAlgebra.ι_range_map_map, CliffordAlgebra.contractRight_algebraMap_mul, CliffordAlgebra.toBaseChange_reverse, CliffordAlgebra.map_id, CliffordAlgebra.contractRight_algebraMap, CliffordAlgebra.contractRight_eq, CliffordAlgebraQuaternion.j_quaternionBasis, CliffordAlgebra.changeForm_comp_changeForm, CliffordAlgebra.mul_ι_mul_ι_of_isOrtho, CliffordAlgebra.foldl_prod_map_ι, CliffordAlgebraComplex.ofComplex_conj, spinGroup.star_eq_inv, CliffordAlgebra.ι_mul_ι_mul_invOf_ι, spinGroup.coe_star_mul_self, CliffordAlgebra.involute_prod_map_ι, pinGroup.coe_star_mul_self, CliffordAlgebra.even.lift.aux_mul, CliffordAlgebraQuaternion.toQuaternion_star, CliffordAlgebra.lift_ι_apply, CliffordAlgebraDualNumber.equiv_symm_eps, CliffordAlgebra.equivOfIsometry_trans, CliffordAlgebra.equivOfIsometry_refl, spinGroup.star_eq_inv', pinGroup.val_inv_toUnits_apply, CliffordAlgebra.contractRight_mul_ι, CliffordAlgebra.op_reverse, CliffordAlgebra.range_lift, CliffordAlgebra.reverse_involute_commute, CliffordAlgebra.foldr_mul, CliffordAlgebra.toProd_comp_ofProd, pinGroup.star_mul_self, CliffordAlgebra.equivBaseChange_symm_apply, CliffordAlgebraQuaternion.toQuaternion_ofQuaternion, CliffordAlgebraComplex.ofComplex_toComplex, CliffordAlgebraComplex.toComplex_comp_ofComplex, CliffordAlgebra.toProd_ι_tmul_one, CliffordAlgebra.changeForm_self_apply, CliffordAlgebra.contractRight_comm, CliffordAlgebra.EquivEven.reverse_e0, CliffordAlgebra.changeFormAux_changeFormAux, CliffordAlgebra.ι_mul_ι_comm, CliffordAlgebra.instNontrivialOfInvertibleOfNat, CliffordAlgebra.ι_range_map_lift, spinGroup.mem_iff, CliffordAlgebra.ι_sq_scalar, CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0, CliffordAlgebra.ofBaseChange_toBaseChange, CliffordAlgebra.foldl_one, CliffordAlgebra.foldl_mul, CliffordAlgebra.changeFormEquiv_symm, spinGroup.coe_mul_star_self, CliffordAlgebra.star_def', CliffordAlgebra.toBaseChange_comp_ofBaseChange, CliffordAlgebra.ι_comp_lift, pinGroup.val_toUnits_apply, CliffordAlgebra.lift_unique, spinGroup.val_inv_toUnits_apply, CliffordAlgebra.foldr_prod_map_ι, CliffordAlgebra.changeFormAux_apply_apply, CliffordAlgebra.toBaseChange_comp_involute, CliffordAlgebra.reverse_involute, CliffordAlgebra.star_def, CliffordAlgebra.evenOdd.gradedMonoid, CliffordAlgebraQuaternion.k_quaternionBasis, CliffordAlgebra.involute_mem_evenOdd_iff, CliffordAlgebra.changeForm_ι_mul, CliffordAlgebra.changeForm_self, CliffordAlgebraQuaternion.i_quaternionBasis, CliffordAlgebra.coe_toEven_reverse_involute, CliffordAlgebra.ι_mul_ι_mul_ι, CliffordAlgebra.reverse_comp_reverse, CliffordAlgebra.adjoin_range_ι, CliffordAlgebra.changeFormEquiv_apply, CliffordAlgebra.EquivEven.neg_e0_mul_v, CliffordAlgebra.range_ι_le_evenOdd_one, CliffordAlgebra.EquivEven.e0_mul_v_mul_e0, CliffordAlgebraComplex.ofComplex_I, TensorAlgebra.toClifford_ι, CliffordAlgebra.hom_ext_iff, CliffordAlgebraQuaternion.equiv_apply, CliffordAlgebra.one_le_evenOdd_zero, CliffordAlgebra.involute_comp_involute, CliffordAlgebra.submodule_comap_mul_reverse, CliffordAlgebra.invOf_ι_mul_ι_mul_ι, CliffordAlgebraQuaternion.equiv_symm_apply, CliffordAlgebra.map_apply_ι, CliffordAlgebra.submodule_map_pow_reverse, CliffordAlgebra.ι_mul_ι_add_swap, CliffordAlgebraQuaternion.ofQuaternion_star, CliffordAlgebra.contractLeft_contractLeft, CliffordAlgebra.evenOdd_map_reverse, CliffordAlgebra.contractLeft_ι_mul, CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion, CliffordAlgebra.comp_ι_sq_scalar, CliffordAlgebra.even.lift_ι, CliffordAlgebra.ι_range_map_reverse, CliffordAlgebra.contractRight_mul_algebraMap, CliffordAlgebra.ι_range_map_involute, CliffordAlgebra.star_smul, pinGroup.star_eq_inv', CliffordAlgebra.even.algHom_ext_iff, CliffordAlgebra.GradedAlgebra.ι_apply, CliffordAlgebra.toEven_comp_ofEven, CliffordAlgebra.reverse.map_mul, CliffordAlgebra.isUnit_ι_iff, CliffordAlgebra.instSMulCommClass, CliffordAlgebra.changeForm_ι_mul_ι, CliffordAlgebra.EquivEven.neg_v_mul_e0, CliffordAlgebra.ι_range_comap_involute, CliffordAlgebra.reverse_prod_map_ι, CliffordAlgebra.reverseOpEquiv_opComm, CliffordAlgebra.contractLeft_comm, CliffordAlgebra.ofBaseChange_tmul_ι, CliffordAlgebra.reverse_reverse, CliffordAlgebra.foldl_algebraMap, CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero, CliffordAlgebra.ofBaseChangeAux_ι, pinGroup.units_mem_iff, CliffordAlgebra.foldr_ι, CliffordAlgebra.changeForm_one, CliffordAlgebra.lift_symm_apply, CliffordAlgebra.foldl_ι, CliffordAlgebraQuaternion.ofQuaternion_mk, CliffordAlgebra.foldl_reverse, spinGroup.mul_star_self, CliffordAlgebra.reverse.commutes, CliffordAlgebra.foldr_one, CliffordAlgebra.toBaseChange_ofBaseChange, CliffordAlgebraComplex.equiv_symm_apply, CliffordAlgebra.reverse_mem_evenOdd_iff, CliffordAlgebra.evenToNeg_ι, QuadraticModuleCat.cliffordAlgebra_map, CliffordAlgebra.map_comp_ι, CliffordAlgebraComplex.toComplex_ι, CliffordAlgebra.changeForm_ι, CliffordAlgebra.foldr_reverse, pinGroup.toUnits_injective, CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho, pinGroup.mul_star_self, CliffordAlgebra.toBaseChange_comp_reverseOp, CliffordAlgebra.EquivEven.v_sq_scalar, pinGroup.star_mem_iff, CliffordAlgebra.contractLeft_ι, CliffordAlgebra.ofEven_comp_toEven, CliffordAlgebra.invOf_ι, CliffordAlgebra.prodEquiv_symm_apply, CliffordAlgebra.contractRight_contractRight, CliffordAlgebra.star_ι, CliffordAlgebra.involute_ι, CliffordAlgebra.even_toSubmodule, CliffordAlgebra.reverse_comp_involute, CliffordAlgebra.prodEquiv_apply, CliffordAlgebra.changeForm_contractLeft, CliffordAlgebra.involute_involute, CliffordAlgebra.involuteEquiv_apply, CliffordAlgebra.even.lift_symm_apply_bilin, CliffordAlgebra.evenEquivEvenNeg_apply, CliffordAlgebraRing.ι_eq_zero, CliffordAlgebraComplex.equiv_apply, CliffordAlgebra.toEven_ι, CliffordAlgebra.equivBaseChange_apply, CliffordAlgebraRing.involute_eq_id, CliffordAlgebra.reverseEquiv_symm_apply, CliffordAlgebra.ofProd_comp_toProd, CliffordAlgebra.submodule_map_mul_reverse, CliffordAlgebra.evenOdd_mul_le, CliffordAlgebra.contractRight_one, CliffordAlgebraDualNumber.equiv_ι, CliffordAlgebra.star_algebraMap, CliffordAlgebra.changeForm_algebraMap, CliffordAlgebra.foldr'Aux_apply_apply, CliffordAlgebra.reverse.map_one, pinGroup.mem_iff, CliffordAlgebra.reverseOp_ι, pinGroup.star_eq_inv, CliffordAlgebra.ι_mul_ι_comm_of_isOrtho, CliffordAlgebra.evenOdd_map_involute, CliffordAlgebra.iSup_ι_range_eq_top, lipschitzGroup.coe_mem_iff_mem, CliffordAlgebra.submodule_comap_pow_reverse, CliffordAlgebra.EquivEven.e0_mul_e0, CliffordAlgebra.contractLeft_mul_algebraMap, CliffordAlgebra.toProd_one_tmul_ι, CliffordAlgebra.even.lift.aux_apply, CliffordAlgebra.toBaseChange_involute, CliffordAlgebra.even.lift.aux_ι, CliffordAlgebra.map_surjective, CliffordAlgebra.contractLeft_algebraMap_mul, CliffordAlgebra.reverseEquiv_apply, CliffordAlgebraRing.reverse_apply, CliffordAlgebraDualNumber.ι_mul_ι, QuadraticModuleCat.cliffordAlgebra_obj_carrier, CliffordAlgebra.EquivEven.involute_e0, CliffordAlgebra.isUnit_ι_of_isUnit, CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion, CliffordAlgebra.evenEquivEvenNeg_symm_apply, CliffordAlgebra.foldr_algebraMap, CliffordAlgebraComplex.toComplex_involute, CliffordAlgebraComplex.toComplex_ofComplex, CliffordAlgebra.lift_comp_ι, CliffordAlgebra.ofEven_ι, CliffordAlgebra.ofBaseChange_tmul_one, CliffordAlgebra.submodule_map_reverse_eq_comap, CliffordAlgebra.toBaseChange_ι, CliffordAlgebra.ι_mem_evenOdd_one, CliffordAlgebraComplex.reverse_eq_id, pinGroup.coe_star, CliffordAlgebra.evenOdd_comap_reverse, CliffordAlgebra.involute_involutive, CliffordAlgebra.EquivEven.reverse_v, CliffordAlgebraComplex.ofComplex_comp_toComplex, CliffordAlgebra.equivOfIsometry_symm, CliffordAlgebra.involuteEquiv_symm_apply, pinGroup.coe_mul_star_self, CliffordAlgebra.ofProd_ι_mk, CliffordAlgebra.GradedAlgebra.lift_ι_eq, CliffordAlgebra.instIsScalarTower, CliffordAlgebra.evenOdd_comap_involute, CliffordAlgebra.contractRight_ι, spinGroup.coe_star, CliffordAlgebraRing.reverse_eq_id, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, CliffordAlgebra.evenToNeg_comp_evenToNeg, CliffordAlgebra.ι_range_comap_reverse, CliffordAlgebra.evenOdd_isCompl, CliffordAlgebraQuaternion.toQuaternion_ι, CliffordAlgebra.reverseOpEquiv_apply, CliffordAlgebra.contractLeftAux_apply_apply, CliffordAlgebra.ofBaseChange_comp_toBaseChange, CliffordAlgebra.contractLeft_one, CliffordAlgebra.equivOfIsometry_apply, CliffordAlgebra.map_comp_map, CliffordAlgebra.leftInverse_map_of_leftInverse, CliffordAlgebra.contractLeftAux_contractLeftAux, CliffordAlgebra.EquivEven.involute_v, spinGroup.toUnits_injective, CliffordAlgebra.reverse_ι, CliffordAlgebra.reverse_involutive, CliffordAlgebra.submodule_map_involute_eq_comap, CliffordAlgebra.changeForm_changeForm, spinGroup.star_mul_self, spinGroup.val_toUnits_apply, CliffordAlgebra.even.lift.aux_one, spinGroup.star_mem_iff, CliffordAlgebra.ι_mul_ι_mul_of_isOrtho, CliffordAlgebra.even.lift.aux_algebraMap, CliffordAlgebraComplex.reverse_apply, CliffordAlgebraQuaternion.ofQuaternion_toQuaternion, CliffordAlgebra.contractLeft_algebraMap
instAlgebraCliffordAlgebra 📖	CompOp	348 math math: CliffordAlgebra.unop_reverseOp, CliffordAlgebra.ι_range_map_map, CliffordAlgebra.contractRight_algebraMap_mul, CliffordAlgebra.toBaseChange_reverse, CliffordAlgebra.map_id, CliffordAlgebra.contractRight_algebraMap, ExteriorAlgebra.isLocalHom_algebraMap, CliffordAlgebra.contractRight_eq, ExteriorAlgebra.GradedAlgebra.liftι_eq, ExteriorAlgebra.ι_eq_algebraMap_iff, exteriorPower.basis_apply, CliffordAlgebraQuaternion.j_quaternionBasis, ExteriorAlgebra.ι_inj, CliffordAlgebra.changeForm_comp_changeForm, CliffordAlgebra.mul_ι_mul_ι_of_isOrtho, CliffordAlgebra.foldl_prod_map_ι, CliffordAlgebraComplex.ofComplex_conj, exteriorPower.linearMap_ext_iff, spinGroup.mem_even, CliffordAlgebra.ι_mul_ι_mul_invOf_ι, CliffordAlgebra.involute_prod_map_ι, ExteriorAlgebra.lift_symm_apply, CliffordAlgebra.even.lift.aux_mul, exteriorPower.coe_basis, exteriorPower.ιMulti_family_linearIndependent_field, CliffordAlgebraQuaternion.toQuaternion_star, exteriorPower.basis_repr_ne, CliffordAlgebra.lift_ι_apply, CliffordAlgebraDualNumber.equiv_symm_eps, ExteriorAlgebra.ιMulti_span_fixedDegree, ExteriorAlgebra.ι_eq_zero_iff, CliffordAlgebra.equivOfIsometry_trans, CliffordAlgebra.equivOfIsometry_refl, ExteriorAlgebra.map_comp_map, CliffordAlgebra.contractRight_mul_ι, CliffordAlgebra.op_reverse, CliffordAlgebra.range_lift, CliffordAlgebra.reverse_involute_commute, exteriorPower.ιMulti_family_span_fixedDegree_of_span, ExteriorAlgebra.liftAlternating_ι_mul, CliffordAlgebra.foldr_mul, ExteriorAlgebra.toTrivSqZeroExt_comp_map, CliffordAlgebra.toProd_comp_ofProd, CliffordAlgebra.equivBaseChange_symm_apply, exteriorPower.alternatingMapLinearEquiv_ιMulti, CliffordAlgebraQuaternion.toQuaternion_ofQuaternion, ExteriorAlgebra.algebraMap_inj, CliffordAlgebraComplex.ofComplex_toComplex, CliffordAlgebraComplex.toComplex_comp_ofComplex, CliffordAlgebra.toProd_ι_tmul_one, CliffordAlgebra.changeForm_self_apply, CliffordAlgebra.contractRight_comm, CliffordAlgebra.EquivEven.reverse_e0, ExteriorAlgebra.algebraMap_eq_one_iff, ExteriorAlgebra.liftAlternating_comp, CliffordAlgebra.changeFormAux_changeFormAux, exteriorPower.ιMulti_span_of_span, CliffordAlgebra.ι_mul_ι_comm, CliffordAlgebra.ι_range_map_lift, spinGroup.mem_iff, CliffordAlgebra.ι_sq_scalar, exteriorPower.alternatingMapLinearEquiv_symm_map, exteriorPower.instFree, ExteriorAlgebra.ιMulti_succ_apply, ExteriorAlgebra.map_comp_ι, ExteriorAlgebra.ιMulti_span, CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0, CliffordAlgebra.ofBaseChange_toBaseChange, CliffordAlgebra.foldl_one, CliffordAlgebra.foldl_mul, CliffordAlgebra.changeFormEquiv_symm, ExteriorAlgebra.map_comp_ιMulti, exteriorPower.ιMultiDual_apply_diag, ExteriorAlgebra.algebraMap_eq_zero_iff, ExteriorAlgebra.lift_ι_apply, ExteriorAlgebra.ιMulti_zero_apply, CliffordAlgebra.star_def', CliffordAlgebra.toBaseChange_comp_ofBaseChange, CliffordAlgebra.ι_comp_lift, CliffordAlgebra.lift_unique, CliffordAlgebra.foldr_prod_map_ι, TensorAlgebra.toExterior_ι, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, CliffordAlgebra.changeFormAux_apply_apply, CliffordAlgebra.toBaseChange_comp_involute, CliffordAlgebra.reverse_involute, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, CliffordAlgebra.star_def, ExteriorAlgebra.lift_comp_ι, CliffordAlgebra.evenOdd.gradedMonoid, CliffordAlgebraQuaternion.k_quaternionBasis, CliffordAlgebra.involute_mem_evenOdd_iff, ExteriorAlgebra.liftAlternating_ιMulti, CliffordAlgebra.changeForm_ι_mul, CliffordAlgebra.changeForm_self, CliffordAlgebraQuaternion.i_quaternionBasis, lipschitzGroup.conjAct_smul_ι_mem_range_ι, ExteriorAlgebra.liftAlternatingEquiv_apply, spinGroup.units_involute_act_eq_conjAct, spinGroup.conjAct_smul_ι_mem_range_ι, CliffordAlgebra.coe_toEven_reverse_involute, ExteriorAlgebra.ι_comp_lift, CliffordAlgebra.ι_mul_ι_mul_ι, spinGroup.involute_act_ι_mem_range_ι, CliffordAlgebra.reverse_comp_reverse, exteriorPower.finrank_eq, CliffordAlgebra.adjoin_range_ι, CliffordAlgebra.changeFormEquiv_apply, spinGroup.conjAct_smul_range_ι, CliffordAlgebra.EquivEven.neg_e0_mul_v, CliffordAlgebra.range_ι_le_evenOdd_one, ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf, exteriorPower.map_apply_ιMulti_family, ExteriorAlgebra.ιMulti_range, exteriorPower.zeroEquiv_naturality, CliffordAlgebra.EquivEven.e0_mul_v_mul_e0, CliffordAlgebraComplex.ofComplex_I, TensorAlgebra.toClifford_ι, CliffordAlgebra.hom_ext_iff, CliffordAlgebraQuaternion.equiv_apply, ExteriorAlgebra.liftAlternating_apply_ιMulti, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, CliffordAlgebra.one_le_evenOdd_zero, CliffordAlgebra.involute_comp_involute, CliffordAlgebra.submodule_comap_mul_reverse, CliffordAlgebra.invOf_ι_mul_ι_mul_ι, CliffordAlgebraQuaternion.equiv_symm_apply, CliffordAlgebra.map_apply_ι, exteriorPower.ιMulti_apply_coe, CliffordAlgebra.submodule_map_pow_reverse, CliffordAlgebra.ι_mul_ι_add_swap, CliffordAlgebraQuaternion.ofQuaternion_star, CliffordAlgebra.contractLeft_contractLeft, CliffordAlgebra.evenOdd_map_reverse, exteriorPower.oneEquiv_naturality, ExteriorAlgebra.ι_range_disjoint_one, CliffordAlgebra.contractLeft_ι_mul, CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion, CliffordAlgebra.comp_ι_sq_scalar, CliffordAlgebra.even.lift_ι, CliffordAlgebra.ι_range_map_reverse, CliffordAlgebra.contractRight_mul_algebraMap, CliffordAlgebra.ι_range_map_involute, ExteriorAlgebra.liftAlternating_one, pinGroup.conjAct_smul_ι_mem_range_ι, CliffordAlgebra.star_smul, CliffordAlgebra.even.algHom_ext_iff, CliffordAlgebra.GradedAlgebra.ι_apply, CliffordAlgebra.toEven_comp_ofEven, CliffordAlgebra.reverse.map_mul, ExteriorAlgebra.ι_sq_zero, CliffordAlgebra.isUnit_ι_iff, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, CliffordAlgebra.changeForm_ι_mul_ι, exteriorPower.ιMultiDual_apply_ιMulti, CliffordAlgebra.EquivEven.neg_v_mul_e0, CliffordAlgebra.ι_range_comap_involute, CliffordAlgebra.reverse_prod_map_ι, CliffordAlgebra.reverseOpEquiv_opComm, exteriorPower.ιMulti_family_eq_coe_comp, exteriorPower.pairingDual_ιMulti_ιMulti, ExteriorAlgebra.map_apply_ι, ExteriorAlgebra.ι_leftInverse, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, CliffordAlgebra.contractLeft_comm, CliffordAlgebra.ofBaseChange_tmul_ι, CliffordAlgebra.reverse_reverse, CliffordAlgebra.foldl_algebraMap, CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero, exteriorPower.oneEquiv_symm_apply, CliffordAlgebra.ofBaseChangeAux_ι, exteriorPower.map_comp_ιMulti, ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower, ExteriorAlgebra.ι_add_mul_swap, CliffordAlgebra.foldr_ι, CliffordAlgebra.changeForm_one, CliffordAlgebra.lift_symm_apply, CliffordAlgebra.foldl_ι, CliffordAlgebraQuaternion.ofQuaternion_mk, pinGroup.conjAct_smul_range_ι, CliffordAlgebra.foldl_reverse, exteriorPower.pairingDual_apply_apply_eq_one, CliffordAlgebra.reverse.commutes, CliffordAlgebra.foldr_one, ExteriorAlgebra.toTrivSqZeroExt_ι, CliffordAlgebra.toBaseChange_ofBaseChange, CliffordAlgebraComplex.equiv_symm_apply, CliffordAlgebra.reverse_mem_evenOdd_iff, CliffordAlgebra.evenToNeg_ι, QuadraticModuleCat.cliffordAlgebra_map, CliffordAlgebra.map_comp_ι, ExteriorAlgebra.isUnit_algebraMap, ExteriorAlgebra.map_injective_field, CliffordAlgebraComplex.toComplex_ι, CliffordAlgebra.changeForm_ι, ExteriorAlgebra.map_injective, CliffordAlgebra.foldr_reverse, exteriorPower.ιMulti_family_span_of_span, CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho, CliffordAlgebra.toBaseChange_comp_reverseOp, exteriorPower.map_injective_field, ExteriorAlgebra.ιMulti_apply, CliffordAlgebra.EquivEven.v_sq_scalar, exteriorPower.alternatingMapLinearEquiv_comp, exteriorPower.basis_coord, CliffordAlgebra.contractLeft_ι, exteriorPower.presentation_relation, CliffordAlgebra.ofEven_comp_toEven, CliffordAlgebra.invOf_ι, CliffordAlgebra.prodEquiv_symm_apply, CliffordAlgebra.contractRight_contractRight, CliffordAlgebra.star_ι, exteriorPower.instFinite, CliffordAlgebra.involute_ι, exteriorPower.alternatingMapToDual_apply_ιMulti, CliffordAlgebra.even_toSubmodule, CliffordAlgebra.reverse_comp_involute, CliffordAlgebra.prodEquiv_apply, CliffordAlgebra.changeForm_contractLeft, CliffordAlgebra.involute_involute, CliffordAlgebra.involuteEquiv_apply, ExteriorAlgebra.map_surjective_iff, CliffordAlgebra.even.lift_symm_apply_bilin, CliffordAlgebra.evenEquivEvenNeg_apply, CliffordAlgebraRing.ι_eq_zero, CliffordAlgebraComplex.equiv_apply, exteriorPower.zeroEquiv_ιMulti, ExteriorAlgebra.liftAlternating_comp_ιMulti, CliffordAlgebra.toEven_ι, CliffordAlgebra.equivBaseChange_apply, CliffordAlgebraRing.involute_eq_id, CliffordAlgebra.reverseEquiv_symm_apply, exteriorPower.map_injective, exteriorPower.basis_repr_apply, exteriorPower.presentation_R, CliffordAlgebra.ofProd_comp_toProd, CliffordAlgebra.submodule_map_mul_reverse, CliffordAlgebra.evenOdd_mul_le, CliffordAlgebra.contractRight_one, CliffordAlgebraDualNumber.equiv_ι, CliffordAlgebra.star_algebraMap, CliffordAlgebra.changeForm_algebraMap, CliffordAlgebra.foldr'Aux_apply_apply, CliffordAlgebra.reverse.map_one, CliffordAlgebra.reverseOp_ι, ExteriorAlgebra.algebraMap_leftInverse, CliffordAlgebra.ι_mul_ι_comm_of_isOrtho, exteriorPower.map_comp_ιMulti_family, CliffordAlgebra.evenOdd_map_involute, exteriorPower.map_id, CliffordAlgebra.iSup_ι_range_eq_top, ExteriorAlgebra.map_apply_ιMulti, CliffordAlgebra.submodule_comap_pow_reverse, CliffordAlgebra.contractLeft_mul_algebraMap, CliffordAlgebra.toProd_one_tmul_ι, CliffordAlgebra.even.lift.aux_apply, CliffordAlgebra.toBaseChange_involute, CliffordAlgebra.even.lift.aux_ι, exteriorPower.pairingDual_apply_apply_eq_one_zero, CliffordAlgebra.map_surjective, ExteriorAlgebra.lift_unique, CliffordAlgebra.contractLeft_algebraMap_mul, CliffordAlgebra.reverseEquiv_apply, CliffordAlgebraRing.reverse_apply, ExteriorAlgebra.hom_ext_iff, ExteriorAlgebra.liftAlternating_algebraMap, ExteriorAlgebra.map_id, pinGroup.involute_act_ι_mem_range_ι, CliffordAlgebraDualNumber.ι_mul_ι, exteriorPower.basis_repr, CliffordAlgebra.EquivEven.involute_e0, CliffordAlgebra.isUnit_ι_of_isUnit, CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion, exteriorPower.alternatingMapLinearEquiv_symm_apply, CliffordAlgebra.evenEquivEvenNeg_symm_apply, CliffordAlgebra.foldr_algebraMap, CliffordAlgebraComplex.toComplex_involute, CliffordAlgebraComplex.toComplex_ofComplex, ExteriorAlgebra.ιInv_comp_map, CliffordAlgebra.lift_comp_ι, CliffordAlgebra.ofEven_ι, exteriorPower.map_apply_ιMulti, CliffordAlgebra.ofBaseChange_tmul_one, CliffordAlgebra.submodule_map_reverse_eq_comap, CliffordAlgebra.toBaseChange_ι, CliffordAlgebra.ι_mem_evenOdd_one, CliffordAlgebraComplex.reverse_eq_id, CliffordAlgebra.evenOdd_comap_reverse, CliffordAlgebra.involute_involutive, ExteriorAlgebra.lhom_ext_iff, ExteriorAlgebra.ι_range_map_map, exteriorPower.map_comp, exteriorPower.ιMultiDual_apply_nondiag, exteriorPower.presentation_var, CliffordAlgebra.EquivEven.reverse_v, CliffordAlgebraComplex.ofComplex_comp_toComplex, CliffordAlgebra.equivOfIsometry_symm, CliffordAlgebra.involuteEquiv_symm_apply, ExteriorAlgebra.comp_ι_sq_zero, exteriorPower.map_surjective, CliffordAlgebra.ofProd_ι_mk, CliffordAlgebra.GradedAlgebra.lift_ι_eq, ExteriorAlgebra.ι_mul_prod_list, ExteriorAlgebra.ιMulti_succ_curryLeft, ExteriorAlgebra.leftInverse_map_iff, exteriorPower.presentation_G, lipschitzGroup.involute_act_ι_mem_range_ι, exteriorPower.ιMulti_family_linearIndependent_ofBasis, CliffordAlgebra.evenOdd_comap_involute, CliffordAlgebra.contractRight_ι, exteriorPower.ιMulti_family_span, exteriorPower.ιMulti_span_fixedDegree, CliffordAlgebraRing.reverse_eq_id, ExteriorAlgebra.GradedAlgebra.ι_apply, ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, exteriorPower.oneEquiv_ιMulti, spinGroup.involute_eq, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, exteriorPower.ιMulti_span, CliffordAlgebra.evenToNeg_comp_evenToNeg, exteriorPower.toTensorPower_apply_ιMulti, CliffordAlgebra.ι_range_comap_reverse, CliffordAlgebra.evenOdd_isCompl, CliffordAlgebraQuaternion.toQuaternion_ι, exteriorPower.zeroEquiv_symm_apply, CliffordAlgebra.reverseOpEquiv_apply, CliffordAlgebra.contractLeftAux_apply_apply, CliffordAlgebra.ofBaseChange_comp_toBaseChange, CliffordAlgebra.contractLeft_one, CliffordAlgebra.equivOfIsometry_apply, CliffordAlgebra.map_comp_map, ExteriorAlgebra.liftAlternating_ι, CliffordAlgebra.leftInverse_map_of_leftInverse, CliffordAlgebra.contractLeftAux_contractLeftAux, lipschitzGroup.conjAct_smul_range_ι, exteriorPower.ιMulti_family_apply_coe, CliffordAlgebra.EquivEven.involute_v, CliffordAlgebra.reverse_ι, CliffordAlgebra.reverse_involutive, CliffordAlgebra.submodule_map_involute_eq_comap, CliffordAlgebra.changeForm_changeForm, exteriorPower.basis_repr_self, CliffordAlgebra.even.lift.aux_one, CliffordAlgebra.ι_mul_ι_mul_of_isOrtho, CliffordAlgebra.even.lift.aux_algebraMap, CliffordAlgebraComplex.reverse_apply, CliffordAlgebraQuaternion.ofQuaternion_toQuaternion, CliffordAlgebra.contractLeft_algebraMap
instInhabitedCliffordAlgebra 📖	CompOp	—
instRingCliffordAlgebra 📖	CompOp	364 math math: CliffordAlgebra.unop_reverseOp, CliffordAlgebra.ι_range_map_map, CliffordAlgebra.contractRight_algebraMap_mul, CliffordAlgebra.toBaseChange_reverse, CliffordAlgebra.map_id, CliffordAlgebra.contractRight_algebraMap, ExteriorAlgebra.isLocalHom_algebraMap, CliffordAlgebra.contractRight_eq, ExteriorAlgebra.GradedAlgebra.liftι_eq, ExteriorAlgebra.ι_eq_algebraMap_iff, exteriorPower.basis_apply, CliffordAlgebraQuaternion.j_quaternionBasis, ExteriorAlgebra.ι_inj, CliffordAlgebra.changeForm_comp_changeForm, CliffordAlgebra.mul_ι_mul_ι_of_isOrtho, CliffordAlgebra.foldl_prod_map_ι, CliffordAlgebraComplex.ofComplex_conj, exteriorPower.linearMap_ext_iff, spinGroup.star_eq_inv, CliffordAlgebra.ι_mul_ι_mul_invOf_ι, spinGroup.coe_star_mul_self, CliffordAlgebra.involute_prod_map_ι, ExteriorAlgebra.lift_symm_apply, pinGroup.coe_star_mul_self, CliffordAlgebra.even.lift.aux_mul, exteriorPower.coe_basis, exteriorPower.ιMulti_family_linearIndependent_field, CliffordAlgebraQuaternion.toQuaternion_star, exteriorPower.basis_repr_ne, CliffordAlgebra.lift_ι_apply, CliffordAlgebraDualNumber.equiv_symm_eps, ExteriorAlgebra.ιMulti_span_fixedDegree, ExteriorAlgebra.ι_eq_zero_iff, CliffordAlgebra.equivOfIsometry_trans, CliffordAlgebra.equivOfIsometry_refl, spinGroup.star_eq_inv', ExteriorAlgebra.map_comp_map, pinGroup.val_inv_toUnits_apply, CliffordAlgebra.contractRight_mul_ι, CliffordAlgebra.op_reverse, CliffordAlgebra.range_lift, CliffordAlgebra.reverse_involute_commute, exteriorPower.ιMulti_family_span_fixedDegree_of_span, ExteriorAlgebra.liftAlternating_ι_mul, CliffordAlgebra.foldr_mul, ExteriorAlgebra.toTrivSqZeroExt_comp_map, CliffordAlgebra.toProd_comp_ofProd, pinGroup.star_mul_self, CliffordAlgebra.equivBaseChange_symm_apply, exteriorPower.alternatingMapLinearEquiv_ιMulti, CliffordAlgebraQuaternion.toQuaternion_ofQuaternion, ExteriorAlgebra.algebraMap_inj, CliffordAlgebraComplex.ofComplex_toComplex, CliffordAlgebraComplex.toComplex_comp_ofComplex, CliffordAlgebra.toProd_ι_tmul_one, CliffordAlgebra.changeForm_self_apply, CliffordAlgebra.contractRight_comm, CliffordAlgebra.EquivEven.reverse_e0, ExteriorAlgebra.algebraMap_eq_one_iff, ExteriorAlgebra.liftAlternating_comp, CliffordAlgebra.changeFormAux_changeFormAux, exteriorPower.ιMulti_span_of_span, CliffordAlgebra.ι_mul_ι_comm, CliffordAlgebra.ι_range_map_lift, spinGroup.mem_iff, CliffordAlgebra.ι_sq_scalar, exteriorPower.alternatingMapLinearEquiv_symm_map, exteriorPower.instFree, ExteriorAlgebra.ιMulti_succ_apply, ExteriorAlgebra.map_comp_ι, ExteriorAlgebra.ιMulti_span, CliffordAlgebra.EquivEven.ι_eq_v_add_smul_e0, CliffordAlgebra.ofBaseChange_toBaseChange, CliffordAlgebra.foldl_one, CliffordAlgebra.foldl_mul, CliffordAlgebra.changeFormEquiv_symm, ExteriorAlgebra.map_comp_ιMulti, exteriorPower.ιMultiDual_apply_diag, ExteriorAlgebra.algebraMap_eq_zero_iff, ExteriorAlgebra.lift_ι_apply, ExteriorAlgebra.ιMulti_zero_apply, spinGroup.coe_mul_star_self, CliffordAlgebra.star_def', CliffordAlgebra.toBaseChange_comp_ofBaseChange, CliffordAlgebra.ι_comp_lift, pinGroup.val_toUnits_apply, CliffordAlgebra.lift_unique, spinGroup.val_inv_toUnits_apply, CliffordAlgebra.foldr_prod_map_ι, TensorAlgebra.toExterior_ι, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, CliffordAlgebra.changeFormAux_apply_apply, CliffordAlgebra.toBaseChange_comp_involute, CliffordAlgebra.reverse_involute, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, CliffordAlgebra.star_def, ExteriorAlgebra.lift_comp_ι, CliffordAlgebra.evenOdd.gradedMonoid, CliffordAlgebraQuaternion.k_quaternionBasis, CliffordAlgebra.involute_mem_evenOdd_iff, ExteriorAlgebra.liftAlternating_ιMulti, CliffordAlgebra.changeForm_ι_mul, CliffordAlgebra.changeForm_self, CliffordAlgebraQuaternion.i_quaternionBasis, ExteriorAlgebra.liftAlternatingEquiv_apply, CliffordAlgebra.coe_toEven_reverse_involute, ExteriorAlgebra.ι_comp_lift, CliffordAlgebra.ι_mul_ι_mul_ι, CliffordAlgebra.reverse_comp_reverse, exteriorPower.finrank_eq, CliffordAlgebra.adjoin_range_ι, CliffordAlgebra.changeFormEquiv_apply, CliffordAlgebra.EquivEven.neg_e0_mul_v, CliffordAlgebra.range_ι_le_evenOdd_one, ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf, exteriorPower.map_apply_ιMulti_family, ExteriorAlgebra.ιMulti_range, exteriorPower.zeroEquiv_naturality, CliffordAlgebra.EquivEven.e0_mul_v_mul_e0, CliffordAlgebraComplex.ofComplex_I, TensorAlgebra.toClifford_ι, CliffordAlgebra.hom_ext_iff, CliffordAlgebraQuaternion.equiv_apply, ExteriorAlgebra.liftAlternating_apply_ιMulti, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, CliffordAlgebra.one_le_evenOdd_zero, CliffordAlgebra.involute_comp_involute, CliffordAlgebra.submodule_comap_mul_reverse, CliffordAlgebra.invOf_ι_mul_ι_mul_ι, CliffordAlgebraQuaternion.equiv_symm_apply, CliffordAlgebra.map_apply_ι, exteriorPower.ιMulti_apply_coe, CliffordAlgebra.submodule_map_pow_reverse, CliffordAlgebra.ι_mul_ι_add_swap, CliffordAlgebraQuaternion.ofQuaternion_star, CliffordAlgebra.contractLeft_contractLeft, CliffordAlgebra.evenOdd_map_reverse, exteriorPower.oneEquiv_naturality, ExteriorAlgebra.ι_range_disjoint_one, CliffordAlgebra.contractLeft_ι_mul, CliffordAlgebraQuaternion.toQuaternion_comp_ofQuaternion, CliffordAlgebra.comp_ι_sq_scalar, CliffordAlgebra.even.lift_ι, CliffordAlgebra.ι_range_map_reverse, CliffordAlgebra.contractRight_mul_algebraMap, CliffordAlgebra.ι_range_map_involute, ExteriorAlgebra.liftAlternating_one, CliffordAlgebra.star_smul, pinGroup.star_eq_inv', CliffordAlgebra.even.algHom_ext_iff, CliffordAlgebra.GradedAlgebra.ι_apply, CliffordAlgebra.toEven_comp_ofEven, CliffordAlgebra.reverse.map_mul, ExteriorAlgebra.ι_sq_zero, CliffordAlgebra.isUnit_ι_iff, CliffordAlgebra.instSMulCommClass, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, CliffordAlgebra.changeForm_ι_mul_ι, exteriorPower.ιMultiDual_apply_ιMulti, CliffordAlgebra.EquivEven.neg_v_mul_e0, CliffordAlgebra.ι_range_comap_involute, CliffordAlgebra.reverse_prod_map_ι, CliffordAlgebra.reverseOpEquiv_opComm, exteriorPower.ιMulti_family_eq_coe_comp, exteriorPower.pairingDual_ιMulti_ιMulti, ExteriorAlgebra.map_apply_ι, ExteriorAlgebra.ι_leftInverse, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, CliffordAlgebra.contractLeft_comm, CliffordAlgebra.ofBaseChange_tmul_ι, CliffordAlgebra.reverse_reverse, CliffordAlgebra.foldl_algebraMap, CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero, exteriorPower.oneEquiv_symm_apply, CliffordAlgebra.ofBaseChangeAux_ι, exteriorPower.map_comp_ιMulti, pinGroup.units_mem_iff, ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower, ExteriorAlgebra.ι_add_mul_swap, CliffordAlgebra.foldr_ι, CliffordAlgebra.changeForm_one, CliffordAlgebra.lift_symm_apply, CliffordAlgebra.foldl_ι, CliffordAlgebraQuaternion.ofQuaternion_mk, CliffordAlgebra.foldl_reverse, spinGroup.mul_star_self, exteriorPower.pairingDual_apply_apply_eq_one, CliffordAlgebra.reverse.commutes, CliffordAlgebra.foldr_one, ExteriorAlgebra.toTrivSqZeroExt_ι, CliffordAlgebra.toBaseChange_ofBaseChange, CliffordAlgebraComplex.equiv_symm_apply, CliffordAlgebra.reverse_mem_evenOdd_iff, CliffordAlgebra.evenToNeg_ι, QuadraticModuleCat.cliffordAlgebra_map, CliffordAlgebra.map_comp_ι, ExteriorAlgebra.isUnit_algebraMap, ExteriorAlgebra.map_injective_field, CliffordAlgebraComplex.toComplex_ι, CliffordAlgebra.changeForm_ι, ExteriorAlgebra.map_injective, CliffordAlgebra.foldr_reverse, exteriorPower.ιMulti_family_span_of_span, pinGroup.toUnits_injective, CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho, pinGroup.mul_star_self, CliffordAlgebra.toBaseChange_comp_reverseOp, exteriorPower.map_injective_field, ExteriorAlgebra.ιMulti_apply, CliffordAlgebra.EquivEven.v_sq_scalar, exteriorPower.alternatingMapLinearEquiv_comp, pinGroup.star_mem_iff, exteriorPower.basis_coord, CliffordAlgebra.contractLeft_ι, exteriorPower.presentation_relation, CliffordAlgebra.ofEven_comp_toEven, CliffordAlgebra.invOf_ι, CliffordAlgebra.prodEquiv_symm_apply, CliffordAlgebra.contractRight_contractRight, CliffordAlgebra.star_ι, exteriorPower.instFinite, CliffordAlgebra.involute_ι, exteriorPower.alternatingMapToDual_apply_ιMulti, CliffordAlgebra.even_toSubmodule, CliffordAlgebra.reverse_comp_involute, CliffordAlgebra.prodEquiv_apply, CliffordAlgebra.changeForm_contractLeft, CliffordAlgebra.involute_involute, CliffordAlgebra.involuteEquiv_apply, ExteriorAlgebra.map_surjective_iff, CliffordAlgebra.even.lift_symm_apply_bilin, CliffordAlgebra.evenEquivEvenNeg_apply, CliffordAlgebraRing.ι_eq_zero, CliffordAlgebraComplex.equiv_apply, exteriorPower.zeroEquiv_ιMulti, ExteriorAlgebra.liftAlternating_comp_ιMulti, CliffordAlgebra.toEven_ι, CliffordAlgebra.equivBaseChange_apply, CliffordAlgebraRing.involute_eq_id, CliffordAlgebra.reverseEquiv_symm_apply, exteriorPower.map_injective, exteriorPower.basis_repr_apply, exteriorPower.presentation_R, CliffordAlgebra.ofProd_comp_toProd, CliffordAlgebra.submodule_map_mul_reverse, CliffordAlgebra.evenOdd_mul_le, CliffordAlgebra.contractRight_one, CliffordAlgebraDualNumber.equiv_ι, CliffordAlgebra.star_algebraMap, CliffordAlgebra.changeForm_algebraMap, CliffordAlgebra.foldr'Aux_apply_apply, CliffordAlgebra.reverse.map_one, pinGroup.mem_iff, CliffordAlgebra.reverseOp_ι, pinGroup.star_eq_inv, ExteriorAlgebra.algebraMap_leftInverse, CliffordAlgebra.ι_mul_ι_comm_of_isOrtho, exteriorPower.map_comp_ιMulti_family, CliffordAlgebra.evenOdd_map_involute, exteriorPower.map_id, CliffordAlgebra.iSup_ι_range_eq_top, lipschitzGroup.coe_mem_iff_mem, ExteriorAlgebra.map_apply_ιMulti, CliffordAlgebra.submodule_comap_pow_reverse, CliffordAlgebra.EquivEven.e0_mul_e0, CliffordAlgebra.contractLeft_mul_algebraMap, CliffordAlgebra.toProd_one_tmul_ι, CliffordAlgebra.even.lift.aux_apply, CliffordAlgebra.toBaseChange_involute, CliffordAlgebra.even.lift.aux_ι, exteriorPower.pairingDual_apply_apply_eq_one_zero, CliffordAlgebra.map_surjective, ExteriorAlgebra.lift_unique, CliffordAlgebra.contractLeft_algebraMap_mul, CliffordAlgebra.reverseEquiv_apply, CliffordAlgebraRing.reverse_apply, ExteriorAlgebra.hom_ext_iff, ExteriorAlgebra.liftAlternating_algebraMap, ExteriorAlgebra.map_id, CliffordAlgebraDualNumber.ι_mul_ι, exteriorPower.basis_repr, CliffordAlgebra.EquivEven.involute_e0, CliffordAlgebra.isUnit_ι_of_isUnit, CliffordAlgebraQuaternion.ofQuaternion_comp_toQuaternion, exteriorPower.alternatingMapLinearEquiv_symm_apply, CliffordAlgebra.evenEquivEvenNeg_symm_apply, CliffordAlgebra.foldr_algebraMap, CliffordAlgebraComplex.toComplex_involute, CliffordAlgebraComplex.toComplex_ofComplex, ExteriorAlgebra.ιInv_comp_map, CliffordAlgebra.lift_comp_ι, CliffordAlgebra.ofEven_ι, exteriorPower.map_apply_ιMulti, CliffordAlgebra.ofBaseChange_tmul_one, CliffordAlgebra.submodule_map_reverse_eq_comap, CliffordAlgebra.toBaseChange_ι, CliffordAlgebra.ι_mem_evenOdd_one, CliffordAlgebraComplex.reverse_eq_id, pinGroup.coe_star, CliffordAlgebra.evenOdd_comap_reverse, CliffordAlgebra.involute_involutive, ExteriorAlgebra.lhom_ext_iff, ExteriorAlgebra.ι_range_map_map, exteriorPower.map_comp, exteriorPower.ιMultiDual_apply_nondiag, exteriorPower.presentation_var, CliffordAlgebra.EquivEven.reverse_v, CliffordAlgebraComplex.ofComplex_comp_toComplex, CliffordAlgebra.equivOfIsometry_symm, CliffordAlgebra.involuteEquiv_symm_apply, pinGroup.coe_mul_star_self, ExteriorAlgebra.comp_ι_sq_zero, exteriorPower.map_surjective, CliffordAlgebra.ofProd_ι_mk, CliffordAlgebra.GradedAlgebra.lift_ι_eq, ExteriorAlgebra.ι_mul_prod_list, ExteriorAlgebra.ιMulti_succ_curryLeft, ExteriorAlgebra.leftInverse_map_iff, exteriorPower.presentation_G, CliffordAlgebra.instIsScalarTower, exteriorPower.ιMulti_family_linearIndependent_ofBasis, CliffordAlgebra.evenOdd_comap_involute, CliffordAlgebra.contractRight_ι, exteriorPower.ιMulti_family_span, exteriorPower.ιMulti_span_fixedDegree, spinGroup.coe_star, CliffordAlgebraRing.reverse_eq_id, ExteriorAlgebra.GradedAlgebra.ι_apply, ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, exteriorPower.oneEquiv_ιMulti, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, exteriorPower.ιMulti_span, CliffordAlgebra.evenToNeg_comp_evenToNeg, exteriorPower.toTensorPower_apply_ιMulti, CliffordAlgebra.ι_range_comap_reverse, CliffordAlgebra.evenOdd_isCompl, CliffordAlgebraQuaternion.toQuaternion_ι, exteriorPower.zeroEquiv_symm_apply, CliffordAlgebra.reverseOpEquiv_apply, CliffordAlgebra.contractLeftAux_apply_apply, CliffordAlgebra.ofBaseChange_comp_toBaseChange, CliffordAlgebra.contractLeft_one, CliffordAlgebra.equivOfIsometry_apply, CliffordAlgebra.map_comp_map, ExteriorAlgebra.liftAlternating_ι, CliffordAlgebra.leftInverse_map_of_leftInverse, CliffordAlgebra.contractLeftAux_contractLeftAux, exteriorPower.ιMulti_family_apply_coe, CliffordAlgebra.EquivEven.involute_v, spinGroup.toUnits_injective, CliffordAlgebra.reverse_ι, CliffordAlgebra.reverse_involutive, CliffordAlgebra.submodule_map_involute_eq_comap, CliffordAlgebra.changeForm_changeForm, exteriorPower.basis_repr_self, spinGroup.star_mul_self, spinGroup.val_toUnits_apply, CliffordAlgebra.even.lift.aux_one, spinGroup.star_mem_iff, CliffordAlgebra.ι_mul_ι_mul_of_isOrtho, CliffordAlgebra.even.lift.aux_algebraMap, CliffordAlgebraComplex.reverse_apply, CliffordAlgebraQuaternion.ofQuaternion_toQuaternion, CliffordAlgebra.contractLeft_algebraMap

---

← Back to Index