Basic

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

Statistics

Metric	Count
Definitions alternatingMapLinearEquiv, map, oneEquiv, presentation, Rels, isPresentationCore, relations, relationsSolutionEquiv, zeroEquiv, ιMulti, ιMulti_family	11
Theorems alternatingMapLinearEquiv_apply_ιMulti, alternatingMapLinearEquiv_comp, alternatingMapLinearEquiv_comp_ιMulti, alternatingMapLinearEquiv_symm_apply, alternatingMapLinearEquiv_symm_map, alternatingMapLinearEquiv_ιMulti, linearMap_ext, linearMap_ext_iff, map_apply_ιMulti, map_apply_ιMulti_family, map_comp, map_comp_ιMulti, map_comp_ιMulti_family, map_id, map_injective, map_injective_field, map_surjective, oneEquiv_naturality, oneEquiv_symm_apply, oneEquiv_ιMulti, relationsSolutionEquiv_apply_apply, relationsSolutionEquiv_symm_apply_var, relations_G, relations_R, relations_relation, presentation_G, presentation_R, presentation_relation, presentation_var, zeroEquiv_naturality, zeroEquiv_symm_apply, zeroEquiv_ιMulti, ιMulti_apply_coe, ιMulti_family_apply_coe, ιMulti_family_eq_coe_comp, ιMulti_family_span, ιMulti_family_span_fixedDegree_of_span, ιMulti_family_span_of_span, ιMulti_span, ιMulti_span_fixedDegree, ιMulti_span_fixedDegree_of_span_eq_top, ιMulti_span_of_span	42
Total	53

exteriorPower

Definitions

Name	Category	Theorems
alternatingMapLinearEquiv 📖	CompOp	6 math math: alternatingMapLinearEquiv_ιMulti, alternatingMapLinearEquiv_symm_map, alternatingMapLinearEquiv_apply_ιMulti, alternatingMapLinearEquiv_comp_ιMulti, alternatingMapLinearEquiv_comp, alternatingMapLinearEquiv_symm_apply
map 📖	CompOp	13 math math: alternatingMapLinearEquiv_symm_map, map_apply_ιMulti_family, zeroEquiv_naturality, oneEquiv_naturality, map_comp_ιMulti, map_injective_field, map_injective, map_comp_ιMulti_family, map_id, map_apply_ιMulti, map_comp, map_surjective, ιMulti_family_span
oneEquiv 📖	CompOp	3 math math: oneEquiv_naturality, oneEquiv_symm_apply, oneEquiv_ιMulti
presentation 📖	CompOp	4 math math: presentation_relation, presentation_R, presentation_var, presentation_G
zeroEquiv 📖	CompOp	3 math math: zeroEquiv_naturality, zeroEquiv_ιMulti, zeroEquiv_symm_apply
ιMulti 📖	CompOp	22 math math: linearMap_ext_iff, alternatingMapLinearEquiv_ιMulti, ιMulti_span_of_span, alternatingMapLinearEquiv_symm_map, ιMulti_apply_coe, alternatingMapLinearEquiv_apply_ιMulti, ιMultiDual_apply_ιMulti, pairingDual_ιMulti_ιMulti, alternatingMapLinearEquiv_comp_ιMulti, oneEquiv_symm_apply, map_comp_ιMulti, pairingDual_apply_apply_eq_one, alternatingMapToDual_apply_ιMulti, zeroEquiv_ιMulti, pairingDual_apply_apply_eq_one_zero, alternatingMapLinearEquiv_symm_apply, map_apply_ιMulti, presentation_var, oneEquiv_ιMulti, ιMulti_span, toTensorPower_apply_ιMulti, zeroEquiv_symm_apply
ιMulti_family 📖	CompOp	15 math math: basis_apply, coe_basis, ιMulti_family_linearIndependent_field, basis_repr_ne, ιMultiDual_apply_diag, map_apply_ιMulti_family, ιMulti_family_eq_coe_comp, ιMulti_family_span_of_span, map_comp_ιMulti_family, basis_repr, ιMultiDual_apply_nondiag, ιMulti_family_linearIndependent_ofBasis, ιMulti_family_span, ιMulti_family_apply_coe, basis_repr_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
alternatingMapLinearEquiv_apply_ιMulti 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap.instFunLike LinearEquiv RingHomInvPair.ids AlternatingMap AlternatingMap.instAddCommMonoid LinearMap.addCommMonoid AlternatingMap.instModuleAddCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv alternatingMapLinearEquiv AlternatingMap.instFunLike ιMulti	—	DFunLike.congr_fun RingHomInvPair.ids smulCommClass_self alternatingMapLinearEquiv_comp_ιMulti
alternatingMapLinearEquiv_comp 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap AddCommGroup.toAddCommMonoid LinearMap ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module AlternatingMap.instAddCommMonoid LinearMap.addCommMonoid AlternatingMap.instModuleAddCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv alternatingMapLinearEquiv LinearMap.compAlternatingMap LinearMap.comp RingHomCompTriple.ids	—	linearMap_ext RingHomInvPair.ids smulCommClass_self RingHomCompTriple.ids AlternatingMap.ext alternatingMapLinearEquiv_comp_ιMulti alternatingMapLinearEquiv_apply_ιMulti
alternatingMapLinearEquiv_comp_ιMulti 📖	mathematical	—	LinearMap.compAlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module DFunLike.coe LinearEquiv RingHom.id RingHomInvPair.ids AlternatingMap LinearMap AlternatingMap.instAddCommMonoid LinearMap.addCommMonoid AlternatingMap.instModuleAddCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv alternatingMapLinearEquiv ιMulti	—	RingHomInvPair.ids smulCommClass_self LinearEquiv.surjective LinearEquiv.symm_apply_apply
alternatingMapLinearEquiv_symm_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AlternatingMap.instFunLike LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap.addCommMonoid AlternatingMap.instAddCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction CommRing.toRing AlternatingMap.instModuleAddCommGroup EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm alternatingMapLinearEquiv LinearMap.compAlternatingMap ιMulti	—	RingHomInvPair.ids smulCommClass_self LinearEquiv.surjective LinearEquiv.symm_apply_apply alternatingMapLinearEquiv_comp_ιMulti
alternatingMapLinearEquiv_symm_map 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup Submodule.module AlternatingMap LinearMap.addCommMonoid AlternatingMap.instAddCommMonoid LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction AlternatingMap.instModuleAddCommGroup EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm alternatingMapLinearEquiv map AlternatingMap.compLinearMap ιMulti	—	RingHomInvPair.ids smulCommClass_self LinearEquiv.symm_apply_apply
alternatingMapLinearEquiv_ιMulti 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids AlternatingMap AddCommGroup.toAddCommMonoid ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup Submodule.module LinearMap Submodule.addCommMonoid AlternatingMap.instAddCommMonoid LinearMap.addCommMonoid AlternatingMap.instModuleAddCommGroup LinearMap.module smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv alternatingMapLinearEquiv ιMulti LinearMap.id	—	linearMap_ext RingHomInvPair.ids smulCommClass_self AlternatingMap.ext alternatingMapLinearEquiv_comp_ιMulti
linearMap_ext 📖	—	LinearMap.compAlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module ιMulti	—	—	Module.Relations.Solution.IsPresentation.postcomp_injective Module.Presentation.toIsPresentation Module.Relations.Solution.ext DFunLike.congr_fun
linearMap_ext_iff 📖	mathematical	—	LinearMap.compAlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module ιMulti	—	linearMap_ext
map_apply_ιMulti 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap.instFunLike map AlternatingMap AlternatingMap.instFunLike ιMulti	—	alternatingMapLinearEquiv_apply_ιMulti
map_apply_ιMulti_family 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module LinearMap.instFunLike map ιMulti_family	—	alternatingMapLinearEquiv_apply_ιMulti
map_comp 📖	mathematical	—	map LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module	—	linearMap_ext RingHomCompTriple.ids AlternatingMap.ext map_comp_ιMulti map_apply_ιMulti
map_comp_ιMulti 📖	mathematical	—	LinearMap.compAlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module map ιMulti AlternatingMap.compLinearMap	—	alternatingMapLinearEquiv_comp_ιMulti
map_comp_ιMulti_family 📖	mathematical	—	Set.Elem Finset Set.powersetCard ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower DFunLike.coe LinearMap RingHom.id Submodule.addCommMonoid Submodule.module LinearMap.instFunLike map ιMulti_family	—	map_apply_ιMulti
map_id 📖	mathematical	—	map LinearMap.id CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module	—	linearMap_ext AlternatingMap.ext map_comp_ιMulti AlternatingMap.compLinearMap_id
map_injective 📖	mathematical	LinearMap.comp CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids LinearMap.id	ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower DFunLike.coe LinearMap Submodule.addCommMonoid Submodule.module LinearMap.instFunLike map	—	RingHomCompTriple.ids Function.RightInverse.injective LinearMap.comp_apply map_comp map_id LinearMap.id_coe
map_injective_field 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	ExteriorAlgebra EuclideanDomain.toCommRing Field.toEuclideanDomain Submodule CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module map	—	map_injective RingHomCompTriple.ids LinearMap.exists_leftInverse_of_injective LinearMap.ker_eq_bot
map_surjective 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike	ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module map	—	RingHomSurjective.ids LinearMap.range_eq_top LinearMap.range_eq_map ιMulti_span Submodule.map_span Set.range_comp LinearMap.coe_compAlternatingMap map_comp_ιMulti AlternatingMap.coe_compLinearMap Set.image_univ Set.range_eq_univ Function.Surjective.comp_left
oneEquiv_naturality 📖	mathematical	—	LinearMap.comp ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids oneEquiv map	—	linearMap_ext RingHomCompTriple.ids RingHomInvPair.ids AlternatingMap.ext map_apply_ιMulti oneEquiv_ιMulti
oneEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm oneEquiv AlternatingMap AlternatingMap.instFunLike ιMulti	—	RingHomInvPair.ids
oneEquiv_ιMulti 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv oneEquiv AlternatingMap AlternatingMap.instFunLike ιMulti	—	RingHomInvPair.ids alternatingMapLinearEquiv_apply_ιMulti
presentation_G 📖	mathematical	—	Module.Relations.G CommRing.toRing Module.Presentation.toRelations ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommGroup Ring.toAddCommGroup Submodule.module presentation	—	—
presentation_R 📖	mathematical	—	Module.Relations.R CommRing.toRing Module.Presentation.toRelations ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommGroup Ring.toAddCommGroup Submodule.module presentation presentation.Rels	—	—
presentation_relation 📖	mathematical	—	Module.Relations.relation CommRing.toRing Module.Presentation.toRelations ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommGroup Ring.toAddCommGroup Submodule.module presentation Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instSub SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Finsupp.instAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Finsupp.single Function.update AddMonoidWithOne.toOne AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	Finsupp.smul_single mul_one
presentation_var 📖	mathematical	—	Module.Relations.Solution.var CommRing.toRing Module.Presentation.toRelations ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommGroup Ring.toAddCommGroup Submodule.module presentation Module.Presentation.toSolution DFunLike.coe AlternatingMap AlternatingMap.instFunLike ιMulti	—	—
zeroEquiv_naturality 📖	mathematical	—	LinearMap.comp ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.module RingHom.id RingHomCompTriple.ids LinearEquiv.toLinearMap RingHomInvPair.ids zeroEquiv map	—	linearMap_ext RingHomCompTriple.ids RingHomInvPair.ids AlternatingMap.ext map_apply_ιMulti zeroEquiv_ιMulti
zeroEquiv_symm_apply 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.addCommMonoid Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm zeroEquiv Submodule.smul Algebra.toSMul Algebra.id RingQuot.instSemiring TensorAlgebra instSemiringTensorAlgebra CliffordAlgebra.Rel AlternatingMap AlternatingMap.instFunLike ιMulti	—	RingHomInvPair.ids
zeroEquiv_ιMulti 📖	mathematical	—	DFunLike.coe LinearEquiv CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids ExteriorAlgebra Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm AddCommGroup.toAddCommMonoid QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Submodule.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv zeroEquiv AlternatingMap AlternatingMap.instFunLike ιMulti AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	RingHomInvPair.ids alternatingMapLinearEquiv_apply_ιMulti Fin.isEmpty'
ιMulti_apply_coe 📖	mathematical	—	ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower DFunLike.coe AlternatingMap Submodule.addCommMonoid Submodule.module AlternatingMap.instFunLike ιMulti ExteriorAlgebra.ιMulti	—	—
ιMulti_family_apply_coe 📖	mathematical	—	ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower ιMulti_family ExteriorAlgebra.ιMulti_family	—	—
ιMulti_family_eq_coe_comp 📖	mathematical	—	ExteriorAlgebra.ιMulti_family Set.Elem Finset Set.powersetCard ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower ιMulti_family	—	—
ιMulti_family_span 📖	mathematical	—	LinearMap.range ExteriorAlgebra Submodule CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.span Set.range Submodule.addCommGroup CommRing.toRing Submodule.module NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra ExteriorAlgebra.exteriorPower Submodule.addCommMonoid RingHom.id RingHomSurjective.ids map Submodule.subtype Set.Elem Finset Set.powersetCard ιMulti_family	—	RingHomSurjective.ids Submodule.subset_span Set.mem_range_self SetLike.coe_injective Set.image_injective Submodule.injective_subtype Submodule.map_coe Submodule.span_image Set.range_comp LinearMap.range_eq_map Submodule.range_subtype ιMulti_family_span_of_span Submodule.map_span map_comp_ιMulti_family
ιMulti_family_span_fixedDegree_of_span 📖	mathematical	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set.range Top.top Submodule Submodule.instTop	ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Set.Elem Finset Set.powersetCard ExteriorAlgebra.ιMulti_family ExteriorAlgebra.exteriorPower	—	le_antisymm Submodule.span_le Set.range_subset_iff SetLike.mem_coe ιMulti_family_eq_coe_comp Submodule.coe_mem ιMulti_span_fixedDegree_of_span_eq_top Set.range_subset_range_iff_exists_comp Set.mem_setOf
ιMulti_family_span_of_span 📖	mathematical	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Set.range Top.top Submodule Submodule.instTop	ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module Set.Elem Finset Set.powersetCard ιMulti_family	—	LinearMap.map_injective RingHomSurjective.ids Submodule.ker_subtype LinearMap.map_span Set.image_univ Set.image_image Set.image_congr Submodule.map_top Submodule.range_subtype ιMulti_family_span_fixedDegree_of_span
ιMulti_span 📖	mathematical	—	Submodule.span ExteriorAlgebra Submodule 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 SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module Set.range DFunLike.coe AlternatingMap AlternatingMap.instFunLike ιMulti Top.top Submodule.instTop	—	LinearMap.map_injective RingHomSurjective.ids Submodule.ker_subtype LinearMap.map_span Set.image_univ Set.image_image Set.image_congr Submodule.map_top Submodule.range_subtype ExteriorAlgebra.ιMulti_span_fixedDegree
ι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 ExteriorAlgebra.ιMulti ExteriorAlgebra.exteriorPower	—	ExteriorAlgebra.ιMulti_span_fixedDegree
ιMulti_span_fixedDegree_of_span_eq_top 📖	mathematical	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Top.top Submodule Submodule.instTop	ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra Set.image DFunLike.coe AlternatingMap AlternatingMap.instFunLike ExteriorAlgebra.ιMulti setOf Set Set.instHasSubset Set.range ExteriorAlgebra.exteriorPower	—	le_antisymm Submodule.span_le ExteriorAlgebra.ιMulti_range ExteriorAlgebra.exteriorPower.eq_1 LinearMap.range_eq_map Submodule.map_span IsScalarTower.right Submodule.span_pow Set.mem_pow Submodule.mem_span_of_mem Set.mem_setOf_eq Set.range_comp Set.image_subset_iff Set.Subset.trans Set.image_subset_preimage_of_inverse ExteriorAlgebra.ι_leftInverse ExteriorAlgebra.ιMulti_apply Set.mem_image
ιMulti_span_of_span 📖	mathematical	Submodule.span CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Top.top Submodule Submodule.instTop	ExteriorAlgebra NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing instRingCliffordAlgebra QuadraticForm QuadraticMap.instZero NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Semiring.toModule Algebra.toModule Ring.toSemiring instAlgebraCliffordAlgebra SetLike.instMembership Submodule.setLike ExteriorAlgebra.exteriorPower Submodule.addCommMonoid Submodule.module Set.image DFunLike.coe AlternatingMap AlternatingMap.instFunLike ιMulti setOf Set Set.instHasSubset Set.range	—	LinearMap.map_injective RingHomSurjective.ids Submodule.ker_subtype LinearMap.map_span Set.image_congr Set.image_image Submodule.map_top Submodule.range_subtype ιMulti_span_fixedDegree_of_span_eq_top

exteriorPower.presentation

Definitions

Name	Category	Theorems
Rels 📖	CompData	2 math math: relations_R, exteriorPower.presentation_R
isPresentationCore 📖	CompOp	—
relations 📖	CompOp	5 math math: relationsSolutionEquiv_symm_apply_var, relationsSolutionEquiv_apply_apply, relations_G, relations_R, relations_relation
relationsSolutionEquiv 📖	CompOp	2 math math: relationsSolutionEquiv_symm_apply_var, relationsSolutionEquiv_apply_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
relationsSolutionEquiv_apply_apply 📖	mathematical	—	DFunLike.coe AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid AlternatingMap.instFunLike Equiv Module.Relations.Solution CommRing.toRing relations EquivLike.toFunLike Equiv.instEquivLike relationsSolutionEquiv Module.Relations.Solution.var	—	—
relationsSolutionEquiv_symm_apply_var 📖	mathematical	—	Module.Relations.Solution.var CommRing.toRing relations DFunLike.coe Equiv AlternatingMap CommSemiring.toSemiring CommRing.toCommSemiring AddCommGroup.toAddCommMonoid Module.Relations.Solution EquivLike.toFunLike Equiv.instEquivLike Equiv.symm relationsSolutionEquiv AlternatingMap.instFunLike	—	—
relations_G 📖	mathematical	—	Module.Relations.G CommRing.toRing relations	—	—
relations_R 📖	mathematical	—	Module.Relations.R CommRing.toRing relations Rels	—	—
relations_relation 📖	mathematical	—	Module.Relations.relation CommRing.toRing relations Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Finsupp.instSub SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup Finsupp.instAdd AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Finsupp.single Function.update AddMonoidWithOne.toOne AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring Module.toDistribMulAction Finsupp.instZero Finsupp.smulZeroClass NonUnitalNonAssocSemiring.toDistribSMul	—	—

---

← Back to Index