Basic

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

Statistics

Metric	Count
Definitions ExteriorAlgebra, algebraMapInv, exteriorPower, invertibleAlgebraMapEquiv, map, toTrivSqZeroExt, «term⋀[_]^_», ι, ιInv, ιMulti, ιMulti_family, toExterior	12
Theorems algebraMap_eq_one_iff, algebraMap_eq_zero_iff, algebraMap_inj, algebraMap_leftInverse, comp_ι_sq_zero, hom_ext, hom_ext_iff, induction, instNontrivial, invertibleAlgebraMapEquiv_apply_invOf, invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, isLocalHom_algebraMap, isUnit_algebraMap, leftInverse_map_iff, lift_comp_ι, lift_symm_apply, lift_unique, lift_ι_apply, map_apply_ι, map_apply_ιMulti, map_comp_map, map_comp_ι, map_comp_ιMulti, map_id, map_injective, map_injective_field, map_surjective_iff, toTrivSqZeroExt_comp_map, toTrivSqZeroExt_ι, ιInv_comp_map, ιMulti_apply, ιMulti_range, ιMulti_span_fixedDegree, ιMulti_succ_apply, ιMulti_succ_curryLeft, ιMulti_zero_apply, ι_add_mul_swap, ι_comp_lift, ι_eq_algebraMap_iff, ι_eq_zero_iff, ι_inj, ι_leftInverse, ι_mul_prod_list, ι_ne_one, ι_range_disjoint_one, ι_range_map_map, ι_sq_zero, toExterior_ι	48
Total	60

ExteriorAlgebra

Definitions

Name	Category	Theorems
algebraMapInv 📖	CompOp	2 math math: invertibleAlgebraMapEquiv_apply_invOf, algebraMap_leftInverse
exteriorPower 📖	CompOp	62 math math: GradedAlgebra.liftι_eq, exteriorPower.basis_apply, exteriorPower.linearMap_ext_iff, exteriorPower.coe_basis, exteriorPower.ιMulti_family_linearIndependent_field, exteriorPower.basis_repr_ne, ιMulti_span_fixedDegree, exteriorPower.ιMulti_family_span_fixedDegree_of_span, exteriorPower.alternatingMapLinearEquiv_ιMulti, exteriorPower.ιMulti_span_of_span, exteriorPower.alternatingMapLinearEquiv_symm_map, exteriorPower.instFree, exteriorPower.ιMultiDual_apply_diag, GradedAlgebra.ι_sq_zero, exteriorPower.finrank_eq, exteriorPower.map_apply_ιMulti_family, ιMulti_range, exteriorPower.zeroEquiv_naturality, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, exteriorPower.ιMulti_apply_coe, exteriorPower.oneEquiv_naturality, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, exteriorPower.ιMultiDual_apply_ιMulti, exteriorPower.ιMulti_family_eq_coe_comp, exteriorPower.pairingDual_ιMulti_ιMulti, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, exteriorPower.oneEquiv_symm_apply, exteriorPower.map_comp_ιMulti, instGradedMonoidNatSubmoduleExteriorPower, exteriorPower.pairingDual_apply_apply_eq_one, exteriorPower.ιMulti_family_span_of_span, exteriorPower.map_injective_field, exteriorPower.alternatingMapLinearEquiv_comp, exteriorPower.basis_coord, exteriorPower.presentation_relation, exteriorPower.instFinite, exteriorPower.alternatingMapToDual_apply_ιMulti, exteriorPower.zeroEquiv_ιMulti, exteriorPower.map_injective, exteriorPower.basis_repr_apply, exteriorPower.presentation_R, exteriorPower.map_comp_ιMulti_family, exteriorPower.map_id, exteriorPower.pairingDual_apply_apply_eq_one_zero, exteriorPower.basis_repr, exteriorPower.alternatingMapLinearEquiv_symm_apply, exteriorPower.map_apply_ιMulti, exteriorPower.map_comp, exteriorPower.ιMultiDual_apply_nondiag, exteriorPower.presentation_var, exteriorPower.map_surjective, exteriorPower.presentation_G, exteriorPower.ιMulti_family_linearIndependent_ofBasis, exteriorPower.ιMulti_family_span, exteriorPower.ιMulti_span_fixedDegree, GradedAlgebra.ι_apply, exteriorPower.oneEquiv_ιMulti, exteriorPower.ιMulti_span, exteriorPower.toTensorPower_apply_ιMulti, exteriorPower.zeroEquiv_symm_apply, exteriorPower.ιMulti_family_apply_coe, exteriorPower.basis_repr_self
invertibleAlgebraMapEquiv 📖	CompOp	2 math math: invertibleAlgebraMapEquiv_apply_invOf, invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot
map 📖	CompOp	13 math math: map_comp_map, toTrivSqZeroExt_comp_map, map_comp_ι, map_comp_ιMulti, map_apply_ι, map_injective_field, map_injective, map_surjective_iff, map_apply_ιMulti, map_id, ιInv_comp_map, ι_range_map_map, leftInverse_map_iff
toTrivSqZeroExt 📖	CompOp	2 math math: toTrivSqZeroExt_comp_map, toTrivSqZeroExt_ι
«term⋀[_]^_» 📖	CompOp	—
ι 📖	CompOp	25 math math: ι_eq_algebraMap_iff, ι_inj, ι_eq_zero_iff, liftAlternating_ι_mul, ιMulti_succ_apply, map_comp_ι, lift_ι_apply, TensorAlgebra.toExterior_ι, lift_comp_ι, ι_comp_lift, ι_range_disjoint_one, ι_sq_zero, map_apply_ι, ι_leftInverse, ι_add_mul_swap, toTrivSqZeroExt_ι, ιMulti_apply, lift_unique, hom_ext_iff, ι_range_map_map, comp_ι_sq_zero, ι_mul_prod_list, ιMulti_succ_curryLeft, GradedAlgebra.ι_apply, liftAlternating_ι
ιInv 📖	CompOp	2 math math: ι_leftInverse, ιInv_comp_map
ιMulti 📖	CompOp	17 math math: ιMulti_span_fixedDegree, ιMulti_succ_apply, ιMulti_span, map_comp_ιMulti, ιMulti_zero_apply, liftAlternatingEquiv_symm_apply, liftAlternating_ιMulti, ιMulti_range, liftAlternating_apply_ιMulti, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, exteriorPower.ιMulti_apply_coe, ιMulti_apply, liftAlternating_comp_ιMulti, map_apply_ιMulti, lhom_ext_iff, ιMulti_succ_curryLeft, exteriorPower.ιMulti_span_fixedDegree
ιMulti_family 📖	CompOp	3 math math: exteriorPower.ιMulti_family_span_fixedDegree_of_span, exteriorPower.ιMulti_family_eq_coe_comp, exteriorPower.ιMulti_family_apply_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_eq_one_iff 📖	mathematical	—	DFunLike.coe RingHom ExteriorAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	map_eq_one_iff MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_leftInverse
algebraMap_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom ExteriorAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_leftInverse
algebraMap_inj 📖	mathematical	—	DFunLike.coe RingHom ExteriorAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra	—	algebraMap_leftInverse
algebraMap_leftInverse 📖	mathematical	—	ExteriorAlgebra DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra Algebra.id AlgHom.funLike algebraMapInv RingHom RingHom.instFunLike algebraMap	—	AlgHom.commutes
comp_ι_sq_zero 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe AlgHom ExteriorAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra AlgHom.funLike LinearMap RingHom.id NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass ι_sq_zero map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass
hom_ext 📖	—	LinearMap.comp ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Semiring.toModule Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap ι	—	—	RingHomCompTriple.ids CliffordAlgebra.hom_ext
hom_ext_iff 📖	mathematical	—	LinearMap.comp ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Semiring.toModule Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap ι	—	RingHomCompTriple.ids hom_ext
induction 📖	—	DFunLike.coe RingHom ExteriorAlgebra Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra LinearMap RingHom.id NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd	—	—	CliffordAlgebra.induction
instNontrivial 📖	mathematical	—	Nontrivial ExteriorAlgebra	—	Function.Injective.nontrivial algebraMap_leftInverse
invertibleAlgebraMapEquiv_apply_invOf 📖	mathematical	—	Invertible.invOf MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring MulOne.toOne DFunLike.coe Equiv Invertible ExteriorAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne RingHom Ring.toSemiring RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing CommRing.toRing EquivLike.toFunLike Equiv.instEquivLike invertibleAlgebraMapEquiv AlgHom Algebra.id AlgHom.funLike algebraMapInv Invertible.map	—	—
invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot 📖	mathematical	—	RingQuot.toQuot TensorAlgebra CommRing.toCommSemiring AddCommGroup.toAddCommMonoid instSemiringTensorAlgebra CliffordAlgebra.Rel QuadraticForm QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Invertible.invOf ExteriorAlgebra MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra MulOne.toOne DFunLike.coe RingHom RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra Equiv Invertible Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing EquivLike.toFunLike Equiv.instEquivLike Equiv.symm invertibleAlgebraMapEquiv RingQuot.Rel instAlgebra Algebra.id IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid Module.toDistribMulAction	—	—
isLocalHom_algebraMap 📖	mathematical	—	IsLocalHom ExteriorAlgebra RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra	—	isLocalHom_of_leftInverse MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass algebraMap_leftInverse
isUnit_algebraMap 📖	mathematical	—	IsUnit ExteriorAlgebra MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring instRingCliffordAlgebra QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule DFunLike.coe RingHom RingHom.instFunLike algebraMap instAlgebraCliffordAlgebra	—	isUnit_map_of_leftInverse MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass algebraMap_leftInverse
leftInverse_map_iff 📖	mathematical	—	ExteriorAlgebra DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra AlgHom.funLike map LinearMap RingHom.id LinearMap.instFunLike	—	map_apply_ι CliffordAlgebra.leftInverse_map_of_leftInverse
lift_comp_ι 📖	mathematical	—	DFunLike.coe Equiv LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom ExteriorAlgebra Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Semiring.toModule instAlgebraCliffordAlgebra EquivLike.toFunLike Equiv.instEquivLike lift LinearMap.comp RingHomCompTriple.ids AlgHom.toLinearMap ι comp_ι_sq_zero	—	CliffordAlgebra.lift_comp_ι
lift_symm_apply 📖	mathematical	—	DFunLike.coe Equiv AlgHom ExteriorAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra LinearMap RingHom.id Algebra.toModule EquivLike.toFunLike Equiv.instEquivLike Equiv.symm lift CliffordAlgebra.lift Equiv.refl	—	—
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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	LinearMap.comp ExteriorAlgebra Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Semiring.toModule instAlgebraCliffordAlgebra RingHomCompTriple.ids AlgHom.toLinearMap ι Equiv AlgHom EquivLike.toFunLike Equiv.instEquivLike lift	—	CliffordAlgebra.lift_unique
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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	AlgHom ExteriorAlgebra Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Semiring.toModule instAlgebraCliffordAlgebra AlgHom.funLike Equiv EquivLike.toFunLike Equiv.instEquivLike lift NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing ι	—	CliffordAlgebra.lift_ι_apply
map_apply_ι 📖	mathematical	—	DFunLike.coe AlgHom ExteriorAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra AlgHom.funLike map LinearMap RingHom.id NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι	—	CliffordAlgebra.map_apply_ι
map_apply_ιMulti 📖	mathematical	—	DFunLike.coe AlgHom ExteriorAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra AlgHom.funLike map AlternatingMap NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule AlternatingMap.instFunLike ιMulti LinearMap RingHom.id LinearMap.instFunLike	—	ιMulti_apply map_list_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass List.map_ofFn map_apply_ι
map_comp_map 📖	mathematical	—	AlgHom.comp ExteriorAlgebra CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra map LinearMap.comp RingHom.id RingHomCompTriple.ids	—	CliffordAlgebra.map_comp_map
map_comp_ι 📖	mathematical	—	LinearMap.comp ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Semiring.toModule Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomCompTriple.ids AlgHom.toLinearMap map ι NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	CliffordAlgebra.map_comp_ι
map_comp_ιMulti 📖	mathematical	—	LinearMap.compAlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Semiring.toModule Algebra.toModule instAlgebraCliffordAlgebra AlgHom.toLinearMap map ιMulti AlternatingMap.compLinearMap NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	AlternatingMap.ext map_apply_ιMulti
map_id 📖	mathematical	—	map LinearMap.id CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AlgHom.id ExteriorAlgebra Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule instAlgebraCliffordAlgebra	—	CliffordAlgebra.map_id
map_injective 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.id	ExteriorAlgebra DFunLike.coe AlgHom Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule instAlgebraCliffordAlgebra AlgHom.funLike map	—	RingHomCompTriple.ids leftInverse_map_iff DFunLike.congr_fun
map_injective_field 📖	mathematical	LinearMap.ker DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring Bot.bot Submodule Submodule.instBot	ExteriorAlgebra EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra AlgHom.funLike map	—	map_injective LinearMap.exists_leftInverse_of_injective
map_surjective_iff 📖	mathematical	—	ExteriorAlgebra DFunLike.coe AlgHom CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule instAlgebraCliffordAlgebra AlgHom.funLike map LinearMap RingHom.id LinearMap.instFunLike	—	RingHomCompTriple.ids LinearMap.comp_apply ιInv_comp_map toTrivSqZeroExt_ι CliffordAlgebra.map_surjective
toTrivSqZeroExt_comp_map 📖	mathematical	—	AlgHom.comp ExteriorAlgebra TrivSqZeroExt CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TrivSqZeroExt.semiring IsScalarTower.to_smulCommClass MulOpposite MulOpposite.instSemiring MulOpposite.instAlgebra Algebra.id IsScalarTower.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup IsScalarTower.left DistribMulAction.toMulAction instAlgebraCliffordAlgebra TrivSqZeroExt.instAlgebra toTrivSqZeroExt map TrivSqZeroExt.map	—	hom_ext IsScalarTower.to_smulCommClass IsScalarTower.op_right IsScalarTower.left LinearMap.ext RingHomCompTriple.ids map_apply_ι toTrivSqZeroExt_ι TrivSqZeroExt.map_inr Zero.instNonempty
toTrivSqZeroExt_ι 📖	mathematical	—	DFunLike.coe AlgHom ExteriorAlgebra TrivSqZeroExt CommRing.toCommSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule TrivSqZeroExt.semiring IsScalarTower.to_smulCommClass MulOpposite MulOpposite.instSemiring MulOpposite.instAlgebra Algebra.id IsScalarTower.op_right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup IsScalarTower.left DistribMulAction.toMulAction instAlgebraCliffordAlgebra TrivSqZeroExt.instAlgebra AlgHom.funLike toTrivSqZeroExt LinearMap RingHom.id NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule LinearMap.instFunLike ι TrivSqZeroExt.inr MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	lift_ι_apply
ιInv_comp_map 📖	mathematical	—	LinearMap.comp ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero Semiring.toModule NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomCompTriple.ids ιInv AlgHom.toLinearMap map	—	RingHomCompTriple.ids mul_comm IsScalarTower.to_smulCommClass IsScalarTower.op_right IsScalarTower.left LinearMap.comp_assoc AlgHom.comp_toLinearMap toTrivSqZeroExt_comp_map TrivSqZeroExt.sndHom_comp_map
ιMulti_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra AlternatingMap.instFunLike ιMulti Distrib.toMul NonUnitalNonAssocSemiring.toDistrib AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne LinearMap RingHom.id LinearMap.instFunLike ι	—	—
ιMulti_range 📖	mathematical	—	Set ExteriorAlgebra Set.instHasSubset Set.range DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra AlternatingMap.instFunLike ιMulti SetLike.coe Submodule Submodule.setLike exteriorPower	—	Set.range_subset_iff ιMulti_apply Submodule.pow_subset_pow Set.mem_pow LinearMap.mem_range_self
ιMulti_span_fixedDegree 📖	mathematical	—	Submodule.span ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Set.range DFunLike.coe AlternatingMap AlternatingMap.instFunLike ιMulti exteriorPower	—	le_antisymm Submodule.span_le ιMulti_range exteriorPower.eq_1 IsScalarTower.right Submodule.pow_eq_span_pow_set Submodule.subset_span Set.mem_pow ιMulti_apply Subtype.prop ι_leftInverse
ιMulti_succ_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra AlternatingMap.instFunLike ιMulti Distrib.toMul NonUnitalNonAssocSemiring.toDistrib LinearMap RingHom.id LinearMap.instFunLike ι Matrix.vecTail	—	—
ιMulti_succ_curryLeft 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AlternatingMap AddCommGroup.toAddCommMonoid ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra AlternatingMap.instAddCommMonoid AlternatingMap.instModule smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction LinearMap.instFunLike AlternatingMap.curryLeft ιMulti LinearMap.compAlternatingMap LinearMap.mulLeft Algebra.to_smulCommClass RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra CliffordAlgebra.Rel ι	—	AlternatingMap.ext smulCommClass_self Algebra.to_smulCommClass ιMulti_succ_apply Matrix.tail_cons
ιMulti_zero_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra AlternatingMap.instFunLike ιMulti AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	—
ι_add_mul_swap 📖	mathematical	—	ExteriorAlgebra Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule Distrib.toMul DFunLike.coe LinearMap RingHom.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho QuadraticMap.IsOrtho.all
ι_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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	LinearMap.comp ExteriorAlgebra Ring.toSemiring instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero Semiring.toModule instAlgebraCliffordAlgebra RingHomCompTriple.ids AlgHom.toLinearMap Equiv AlgHom EquivLike.toFunLike Equiv.instEquivLike lift ι	—	CliffordAlgebra.ι_comp_lift
ι_eq_algebraMap_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ExteriorAlgebra AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι RingHom RingHom.instFunLike algebraMap NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	mul_comm IsScalarTower.to_smulCommClass IsScalarTower.op_right IsScalarTower.left toTrivSqZeroExt_ι AlgHom.commutes map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ι_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ExteriorAlgebra AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass LinearMap.semilinearMapClass
ι_inj 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ExteriorAlgebra AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι	—	ι_leftInverse
ι_leftInverse 📖	mathematical	—	ExteriorAlgebra DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ιInv ι	—	toTrivSqZeroExt_ι
ι_mul_prod_list 📖	mathematical	—	ExteriorAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	mul_assoc ι_sq_zero MulZeroClass.zero_mul eq_zero_iff_eq_zero_of_add_eq_zero add_mul Distrib.rightDistribClass ι_add_mul_swap MulZeroClass.mul_zero
ι_ne_one 📖	—	—	—	—	RingHom.map_one ι_eq_algebraMap_iff one_ne_zero NeZero.one
ι_range_disjoint_one 📖	mathematical	—	Disjoint Submodule ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Submodule.instPartialOrder Submodule.instOrderBot LinearMap.range RingHom.id RingHomSurjective.ids ι Submodule.one	—	RingHomSurjective.ids Submodule.disjoint_def Submodule.mem_one ι_eq_algebraMap_iff map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
ι_range_map_map 📖	mathematical	—	Submodule.map ExteriorAlgebra CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Ring.toSemiring instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero Semiring.toModule Algebra.toModule instAlgebraCliffordAlgebra RingHom.id RingHomSurjective.ids AlgHom.toLinearMap map LinearMap.range ι NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	CliffordAlgebra.ι_range_map_map
ι_sq_zero 📖	mathematical	—	ExteriorAlgebra Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm CommRing.toCommSemiring AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Semiring.toModule DFunLike.coe LinearMap RingHom.id Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra LinearMap.instFunLike ι MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	CliffordAlgebra.ι_sq_scalar map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass

TensorAlgebra

Definitions

Name	Category	Theorems
toExterior 📖	CompOp	1 math math: toExterior_ι

Theorems

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

(root)

Definitions

Name	Category	Theorems
ExteriorAlgebra 📖	CompOp	117 math math: ExteriorAlgebra.isLocalHom_algebraMap, ExteriorAlgebra.GradedAlgebra.liftι_eq, ExteriorAlgebra.ι_eq_algebraMap_iff, exteriorPower.basis_apply, ExteriorAlgebra.ι_inj, exteriorPower.linearMap_ext_iff, ExteriorAlgebra.lift_symm_apply, exteriorPower.coe_basis, exteriorPower.ιMulti_family_linearIndependent_field, exteriorPower.basis_repr_ne, ExteriorAlgebra.ιMulti_span_fixedDegree, ExteriorAlgebra.ι_eq_zero_iff, ExteriorAlgebra.map_comp_map, exteriorPower.ιMulti_family_span_fixedDegree_of_span, ExteriorAlgebra.liftAlternating_ι_mul, ExteriorAlgebra.toTrivSqZeroExt_comp_map, exteriorPower.alternatingMapLinearEquiv_ιMulti, ExteriorAlgebra.algebraMap_inj, ExteriorAlgebra.algebraMap_eq_one_iff, ExteriorAlgebra.liftAlternating_comp, exteriorPower.ιMulti_span_of_span, exteriorPower.alternatingMapLinearEquiv_symm_map, exteriorPower.instFree, ExteriorAlgebra.ιMulti_succ_apply, ExteriorAlgebra.map_comp_ι, ExteriorAlgebra.ιMulti_span, ExteriorAlgebra.map_comp_ιMulti, exteriorPower.ιMultiDual_apply_diag, ExteriorAlgebra.algebraMap_eq_zero_iff, ExteriorAlgebra.lift_ι_apply, ExteriorAlgebra.ιMulti_zero_apply, TensorAlgebra.toExterior_ι, ExteriorAlgebra.liftAlternatingEquiv_symm_apply, ExteriorAlgebra.GradedAlgebra.ι_sq_zero, ExteriorAlgebra.lift_comp_ι, ExteriorAlgebra.liftAlternating_ιMulti, ExteriorAlgebra.liftAlternatingEquiv_apply, ExteriorAlgebra.ι_comp_lift, exteriorPower.finrank_eq, ExteriorAlgebra.invertibleAlgebraMapEquiv_apply_invOf, exteriorPower.map_apply_ιMulti_family, ExteriorAlgebra.ιMulti_range, exteriorPower.zeroEquiv_naturality, ExteriorAlgebra.liftAlternating_apply_ιMulti, exteriorPower.ιMulti_span_fixedDegree_of_span_eq_top, exteriorPower.ιMulti_apply_coe, exteriorPower.oneEquiv_naturality, ExteriorAlgebra.ι_range_disjoint_one, ExteriorAlgebra.liftAlternating_one, ExteriorAlgebra.ι_sq_zero, exteriorPower.alternatingMapLinearEquiv_apply_ιMulti, exteriorPower.ιMultiDual_apply_ιMulti, exteriorPower.ιMulti_family_eq_coe_comp, exteriorPower.pairingDual_ιMulti_ιMulti, ExteriorAlgebra.map_apply_ι, ExteriorAlgebra.ι_leftInverse, exteriorPower.alternatingMapLinearEquiv_comp_ιMulti, exteriorPower.oneEquiv_symm_apply, exteriorPower.map_comp_ιMulti, ExteriorAlgebra.instGradedMonoidNatSubmoduleExteriorPower, ExteriorAlgebra.ι_add_mul_swap, exteriorPower.pairingDual_apply_apply_eq_one, ExteriorAlgebra.toTrivSqZeroExt_ι, ExteriorAlgebra.isUnit_algebraMap, ExteriorAlgebra.map_injective_field, ExteriorAlgebra.instNontrivial, ExteriorAlgebra.map_injective, exteriorPower.ιMulti_family_span_of_span, exteriorPower.map_injective_field, ExteriorAlgebra.ιMulti_apply, exteriorPower.alternatingMapLinearEquiv_comp, exteriorPower.basis_coord, exteriorPower.presentation_relation, exteriorPower.instFinite, exteriorPower.alternatingMapToDual_apply_ιMulti, ExteriorAlgebra.map_surjective_iff, exteriorPower.zeroEquiv_ιMulti, ExteriorAlgebra.liftAlternating_comp_ιMulti, exteriorPower.map_injective, exteriorPower.basis_repr_apply, exteriorPower.presentation_R, ExteriorAlgebra.algebraMap_leftInverse, exteriorPower.map_comp_ιMulti_family, exteriorPower.map_id, ExteriorAlgebra.map_apply_ιMulti, exteriorPower.pairingDual_apply_apply_eq_one_zero, ExteriorAlgebra.lift_unique, ExteriorAlgebra.hom_ext_iff, ExteriorAlgebra.liftAlternating_algebraMap, ExteriorAlgebra.map_id, exteriorPower.basis_repr, exteriorPower.alternatingMapLinearEquiv_symm_apply, ExteriorAlgebra.ιInv_comp_map, exteriorPower.map_apply_ιMulti, ExteriorAlgebra.lhom_ext_iff, ExteriorAlgebra.ι_range_map_map, exteriorPower.map_comp, exteriorPower.ιMultiDual_apply_nondiag, exteriorPower.presentation_var, ExteriorAlgebra.comp_ι_sq_zero, exteriorPower.map_surjective, ExteriorAlgebra.ι_mul_prod_list, ExteriorAlgebra.ιMulti_succ_curryLeft, ExteriorAlgebra.leftInverse_map_iff, exteriorPower.presentation_G, exteriorPower.ιMulti_family_linearIndependent_ofBasis, exteriorPower.ιMulti_family_span, exteriorPower.ιMulti_span_fixedDegree, ExteriorAlgebra.GradedAlgebra.ι_apply, ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot, exteriorPower.oneEquiv_ιMulti, exteriorPower.ιMulti_span, exteriorPower.toTensorPower_apply_ιMulti, exteriorPower.zeroEquiv_symm_apply, ExteriorAlgebra.liftAlternating_ι, exteriorPower.ιMulti_family_apply_coe, exteriorPower.basis_repr_self

---

← Back to Index