VectorSpace

📁 Source: Mathlib/LinearAlgebra/Basis/VectorSpace.lean

Statistics

Metric	Count
Definitions leftInverse, extend, extendLe, ofSpan, ofVectorSpace, ofVectorSpaceIndex, sumExtend, sumExtendIndex	8
Theorems exists_extend, exists_extend_of_notMem, exists_leftInverse_of_injective, leftInverse_apply_of_inj, leftInverse_comp_of_inj, coe_extend, coe_extendLe, coe_ofSpan, coe_ofVectorSpace, exists_basis, extendLe_apply_self, extendLe_subset, extend_apply_self, ofSpan_apply_self, ofSpan_subset, linearIndependent, ofVectorSpace_apply_self, range_extend, range_extendLe, range_ofSpan, range_ofVectorSpace, subset_extend, subset_extendLe, of_divisionRing, complementedLattice, exists_isCompl, exists_le_ker_of_lt_top, exists_le_ker_of_notMem, card_fintype, atom_iff_nonzero_span, exists_basis_of_pairing_eq_zero, exists_basis_of_pairing_ne_zero, instIsAtomisticSubmodule, instNontrivialLinearMapId, nonzero_span_atom, quotient_prod_linearEquiv	36
Total	44

LinearMap

Definitions

Name	Category	Theorems
leftInverse 📖	CompOp	2 math math: leftInverse_comp_of_inj, leftInverse_apply_of_inj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_extend 📖	mathematical	—	comp Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Submodule.subtype	—	RingHomCompTriple.ids exists_leftInverse_of_injective Submodule.ker_subtype comp_assoc comp_id
exists_extend_of_notMem 📖	mathematical	Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike	comp Submodule.addCommMonoid Submodule.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Submodule.subtype DFunLike.coe LinearMap instFunLike	—	RingHomCompTriple.ids exists_extend ext Submodule.mem_sup_left LinearPMap.supSpanSingleton_apply_mk_of_mem Subtype.coe_eta Submodule.mem_sup_right Submodule.mem_span_singleton_self LinearPMap.supSpanSingleton_apply_self
exists_leftInverse_of_injective 📖	mathematical	ker DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring Bot.bot Submodule Submodule.instBot	comp RingHomCompTriple.ids id	—	LinearIndependent.linearIndepOn_id Module.Basis.linearIndependent LinearIndepOn.image Module.Basis.coe_ofVectorSpace Subtype.range_coe_subtype Module.Basis.range_ofVectorSpace Set.subset_univ LinearIndepOn.subset_extend RingHomCompTriple.ids RingHomInvPair.ids AddMonoid.nat_smulCommClass' Module.Basis.ext Set.image_subset_iff Module.Basis.extend_apply_self Module.Basis.ofVectorSpace_apply_self Module.Basis.constr_basis Function.leftInverse_invFun ker_eq_bot
leftInverse_apply_of_inj 📖	mathematical	ker DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring Bot.bot Submodule Submodule.instBot	DFunLike.coe LinearMap instFunLike leftInverse	—	RingHomCompTriple.ids ext_iff
leftInverse_comp_of_inj 📖	mathematical	ker DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring Bot.bot Submodule Submodule.instBot	comp RingHomCompTriple.ids leftInverse id	—	RingHomCompTriple.ids exists_leftInverse_of_injective comp.congr_simp

Module.Basis

Definitions

Name	Category	Theorems
extend 📖	CompOp	3 math math: range_extend, extend_apply_self, coe_extend
extendLe 📖	CompOp	5 math math: coe_extendLe, extendLe_subset, range_extendLe, subset_extendLe, extendLe_apply_self
ofSpan 📖	CompOp	4 math math: ofSpan_subset, range_ofSpan, ofSpan_apply_self, coe_ofSpan
ofVectorSpace 📖	CompOp	4 math math: range_ofVectorSpace, FGModuleCat.FGModuleCatCoevaluation_apply_one, coe_ofVectorSpace, ofVectorSpace_apply_self
ofVectorSpaceIndex 📖	CompOp	9 math math: ofVectorSpaceIndex.linearIndependent, range_ofVectorSpace, IsNoetherian.range_finsetBasis, FGModuleCat.FGModuleCatCoevaluation_apply_one, coe_ofVectorSpace, IsNoetherian.coe_finsetBasisIndex, ofVectorSpace_apply_self, IsNoetherian.coeSort_finsetBasisIndex, finite_ofVectorSpaceIndex_of_rank_lt_aleph0
sumExtend 📖	CompOp	—
sumExtendIndex 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_extend 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	DFunLike.coe Module.Basis Set.Elem LinearIndepOn.extend Set.univ Set.subset_univ instFunLike extend Set Set.instMembership	—	Set.subset_univ extend_apply_self
coe_extendLe 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set Set.instHasSubset Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	DFunLike.coe Module.Basis Set.Elem LinearIndepOn.extend instFunLike extendLe Set.instMembership	—	extendLe_apply_self
coe_ofSpan 📖	mathematical	Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	DFunLike.coe Module.Basis Set.Elem LinearIndepOn.extend Set Set.instEmptyCollection linearIndepOn_empty Set.empty_subset instFunLike ofSpan Set.instMembership	—	linearIndepOn_empty Set.empty_subset ofSpan_apply_self
coe_ofVectorSpace 📖	mathematical	—	DFunLike.coe Module.Basis Set.Elem ofVectorSpaceIndex DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid instFunLike ofVectorSpace Set Set.instMembership	—	ofVectorSpace_apply_self
exists_basis 📖	mathematical	—	Module.Basis Set.Elem DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	—
extendLe_apply_self 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set Set.instHasSubset Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	DFunLike.coe Module.Basis Set.Elem LinearIndepOn.extend instFunLike extendLe Set.instMembership	—	mk_apply
extendLe_subset 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set Set.instHasSubset Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	Set.range Set.Elem LinearIndepOn.extend DFunLike.coe Module.Basis instFunLike extendLe	—	LinearIndepOn.extend_subset range_extendLe
extend_apply_self 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	DFunLike.coe Module.Basis Set.Elem LinearIndepOn.extend Set.univ Set.subset_univ instFunLike extend Set Set.instMembership	—	Set.subset_univ mk_apply
ofSpan_apply_self 📖	mathematical	Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	DFunLike.coe Module.Basis Set.Elem LinearIndepOn.extend Set Set.instEmptyCollection linearIndepOn_empty Set.empty_subset instFunLike ofSpan Set.instMembership	—	linearIndepOn_empty Set.empty_subset extendLe_apply_self linearIndependent_empty
ofSpan_subset 📖	mathematical	Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	Set Set.instHasSubset Set.range Set.Elem LinearIndepOn.extend Set.instEmptyCollection linearIndepOn_empty Set.empty_subset DFunLike.coe Module.Basis instFunLike ofSpan	—	extendLe_subset linearIndependent_empty Set.empty_subset
ofVectorSpace_apply_self 📖	mathematical	—	DFunLike.coe Module.Basis Set.Elem ofVectorSpaceIndex DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid instFunLike ofVectorSpace Set Set.instMembership	—	mk_apply Set.subset_univ
range_extend 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	Set.range Set.Elem LinearIndepOn.extend Set.univ Set.subset_univ DFunLike.coe Module.Basis instFunLike extend	—	Set.subset_univ coe_extend Subtype.range_coe_subtype Set.setOf_mem_eq
range_extendLe 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set Set.instHasSubset Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	Set.range Set.Elem LinearIndepOn.extend DFunLike.coe Module.Basis instFunLike extendLe	—	coe_extendLe Subtype.range_coe_subtype Set.setOf_mem_eq
range_ofSpan 📖	mathematical	Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	Set.range Set.Elem LinearIndepOn.extend Set Set.instEmptyCollection linearIndepOn_empty Set.empty_subset DFunLike.coe Module.Basis instFunLike ofSpan	—	linearIndepOn_empty Set.empty_subset coe_ofSpan Subtype.range_coe_subtype Set.setOf_mem_eq
range_ofVectorSpace 📖	mathematical	—	Set.range Set.Elem ofVectorSpaceIndex DFunLike.coe Module.Basis DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid instFunLike ofVectorSpace	—	range_extend
subset_extend 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	Set Set.instHasSubset LinearIndepOn.extend Set.univ Set.subset_univ	—	LinearIndepOn.subset_extend Set.subset_univ
subset_extendLe 📖	mathematical	LinearIndepOn DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Set Set.instHasSubset Submodule Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop Submodule.span	Set.range Set.Elem LinearIndepOn.extend DFunLike.coe Module.Basis instFunLike extendLe	—	LinearIndepOn.subset_extend range_extendLe

Module.Basis.ofVectorSpaceIndex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
linearIndependent 📖	mathematical	—	LinearIndependent Set Set.instMembership Module.Basis.ofVectorSpaceIndex DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	Module.Basis.ofVectorSpace_apply_self Module.Basis.linearIndependent

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_divisionRing 📖	mathematical	—	Module.Free DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid	—	of_basis

Submodule

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
complementedLattice 📖	mathematical	—	ComplementedLattice Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice CompleteLattice.toBoundedOrder	—	exists_isCompl
exists_isCompl 📖	mathematical	—	IsCompl Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid instPartialOrder CompleteLattice.toBoundedOrder completeLattice	—	LinearMap.isCompl_of_proj ker_subtype
exists_le_ker_of_lt_top 📖	mathematical	Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Preorder.toLT PartialOrder.toPreorder instPartialOrder Top.top instTop	Preorder.toLE LinearMap.ker NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring	—	SetLike.exists_of_lt instIsConcreteLE exists_le_ker_of_notMem
exists_le_ker_of_notMem 📖	mathematical	Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing DivisionRing.toRing Semiring.toModule RingHom.id Semiring.toNonAssocSemiring	—	RingHomCompTriple.ids LinearMap.exists_extend_of_notMem NeZero.one DivisionRing.toNontrivial

VectorSpace

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_fintype 📖	mathematical	—	Fintype.card Monoid.toNatPow Nat.instMonoid	—	Module.card_fintype

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
atom_iff_nonzero_span 📖	mathematical	—	IsAtom Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instOrderBot Submodule.span Set Set.instSingletonSet	—	Submodule.ne_bot_iff lt_iff_le_and_ne Submodule.span_singleton_eq_bot Submodule.span_singleton_le_iff_mem nonzero_span_atom
exists_basis_of_pairing_eq_zero 📖	mathematical	DFunLike.coe LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Semiring.toModule LinearMap.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	Module.Basis Set.Elem Module.Basis.instFunLike Module.Basis.coord	—	CanLift.prf Subtype.canLift Field.isDomain Submodule.instIsTorsionFree DivisionSemiring.to_moduleIsTorsionFree AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass Set.subset_univ map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass inv_mul_cancel₀ RingHomSurjective.ids Submodule.span_image Submodule.map.congr_simp Module.Basis.span_eq Submodule.map_top Submodule.range_subtype Module.Basis.coe_extend Subtype.range_coe_subtype LinearIndepOn.subset_extend LinearIndepOn.id_insert LinearIndepOn.image LinearIndependent.linearIndepOn_id Module.Basis.linearIndependent Submodule.ker_subtype NeZero.one DivisionRing.toNontrivial neg_smul map_add SemilinearMapClass.toAddHomClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass mul_one add_neg_cancel LinearMap.map_coe_ker Module.Basis.ext RingHomInvPair.ids Module.Basis.coord_apply Module.Basis.repr_self Module.Basis.mk_apply Finsupp.single_eq_same Finsupp.single_eq_of_ne'
exists_basis_of_pairing_ne_zero 📖	mathematical	—	DFunLike.coe Module.Basis Set.Elem DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AddCommGroup.toAddCommMonoid Module.Basis.instFunLike LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule LinearMap.instSMul instDistribSMul NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Field.toCommRing Algebra.to_smulCommClass Semifield.toCommSemiring CommSemiring.toSemiring Algebra.id LinearMap.instFunLike Module.Basis.coord	—	RingHomSurjective.ids Submodule.span_image Submodule.map.congr_simp Module.Basis.span_eq Submodule.map_top Submodule.range_subtype LinearIndepOn.id_insert LinearIndepOn.image LinearIndependent.linearIndepOn_id Module.Basis.linearIndependent Submodule.ker_subtype map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass map_smul SemilinearMapClass.toMulActionSemiHomClass Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.subst_add Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.eval_cons_mul_eval one_mul Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst div_one neg_div neg_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ mul_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons_zero Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero mul_neg Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one one_ne_zero NeZero.one GroupWithZero.toNontrivial Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Subtype.range_coe_subtype Set.mem_insert Algebra.to_smulCommClass Module.Basis.ext RingHomInvPair.ids Module.Basis.repr_self Finsupp.single_eq_same LinearMap.mem_ker Submodule.subset_span Set.mem_insert_iff Subtype.prop Finsupp.single_eq_of_ne MulZeroClass.mul_zero
instIsAtomisticSubmodule 📖	mathematical	—	IsAtomistic Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid Submodule.instPartialOrder Submodule.instOrderBot	—	CompleteLattice.isAtomistic_iff Submodule.submodule_eq_sSup_le_nonzero_spans nonzero_span_atom
instNontrivialLinearMapId 📖	mathematical	—	Nontrivial LinearMap DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid	—	exists_ne RingHomCompTriple.ids LinearMap.exists_extend_of_notMem DFunLike.ne_iff
nonzero_span_atom 📖	mathematical	—	IsAtom Submodule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring AddCommGroup.toAddCommMonoid PartialOrder.toPreorder Submodule.instPartialOrder Submodule.instOrderBot Submodule.span Set Set.instSingletonSet	—	Submodule.ne_bot_iff Submodule.mem_span_singleton_self Submodule.mem_span_singleton eq_or_ne zero_smul Submodule.smul_mem_iff IsScalarTower.left
quotient_prod_linearEquiv 📖	mathematical	—	LinearEquiv DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient DivisionRing.toRing SetLike.instMembership Submodule.setLike Prod.instAddCommMonoid Submodule.Quotient.addCommGroup Submodule.addCommMonoid Prod.instModule Submodule.Quotient.module Submodule.module	—	RingHomInvPair.ids Submodule.exists_isCompl RingHomCompTriple.ids IsCompl.symm

---

← Back to Index