Basic

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

Statistics

Metric	Count
Definitions equiv, fintype, restrictScalarsEquiv, fintype, unique, comapMkQOrderEmbedding, comapMkQRelIso, factor, liftQ, liftQSpanSingleton, mapQ, mapQLinear, quotEquivOfEqBot	13
Theorems ker_le_range_iff, range_eq_top_of_cancel, range_mkQ_comp, equiv_apply, equiv_refl, equiv_symm, equiv_symm_apply, equiv_trans, instSubsingletonQuotient, nontrivial_iff, nontrivial_of_lt_top, nontrivial_of_ne_top, restrictScalarsEquiv_mk, restrictScalarsEquiv_symm_mk, subsingleton_iff, infinite, coe_quotEquivOfEqBot_symm, comapMkQOrderEmbedding_eq, comap_liftQ, comap_map_mkQ, factor_comp, factor_comp_apply, factor_comp_mk, factor_mk, factor_surjective, ker_liftQ, ker_liftQ_eq_bot, ker_liftQ_eq_bot', ker_mkQ, le_comap_mkQ, liftQSpanSingleton_apply, liftQ_apply, liftQ_mkQ, mapQ_apply, mapQ_comp, mapQ_id, mapQ_mkQ, mapQ_pow, mapQ_zero, map_liftQ, map_mkQ_eq_top, mkQ_map_self, pi_liftQ_eq_liftQ_pi, quotEquivOfEqBot_apply_mk, quotEquivOfEqBot_symm_apply, range_liftQ, range_mkQ, span_preimage_eq, strictMono_comap_prod_map, subsingleton_quotient_iff_eq_top, unique_quotient_iff_eq_top	51
Total	64

LinearMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ker_le_range_iff 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder ker range comp SetLike.instMembership Submodule.setLike HasQuotient.Quotient Submodule.hasQuotient Submodule.addCommMonoid Submodule.Quotient.addCommGroup Submodule.module Submodule.Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids Submodule.mkQ Submodule.subtype LinearMap instZero	—	RingHomCompTriple.ids RingHomSurjective.ids range_le_ker_iff Submodule.ker_mkQ Submodule.range_subtype
range_eq_top_of_cancel 📖	mathematical	—	range Ring.toSemiring AddCommGroup.toAddCommMonoid Top.top Submodule Submodule.instTop	—	RingHomCompTriple.right_ids zero_comp Submodule.ker_mkQ range_mkQ_comp ker_zero
range_mkQ_comp 📖	mathematical	—	comp HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient range Submodule.Quotient.addCommGroup Submodule.Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.right_ids Submodule.mkQ LinearMap instZero	—	ext RingHomCompTriple.right_ids

Submodule

Definitions

Name	Category	Theorems
comapMkQOrderEmbedding 📖	CompOp	1 math math: comapMkQOrderEmbedding_eq
comapMkQRelIso 📖	CompOp	—
factor 📖	CompOp	9 math math: factor_mk, AdicCompletion.factor_eval_eq_evalₐ, factor_eq_factor, factor_comp, mapQ_eq_factor, AdicCompletion.factor_eval_liftRingHom, factor_comp_apply, factor_comp_mk, factor_surjective
liftQ 📖	CompOp	14 math math: LinearMap.surjective_range_liftQ, ker_liftQ_eq_bot', LinearMap.injective_range_liftQ_of_exact, pi_liftQ_eq_liftQ_pi, ker_liftQ_eq_bot, CategoryTheory.ShortComplex.moduleCatLeftHomologyData_descH_hom, liftQ_apply, map_liftQ, Function.Exact.linearEquivOfSurjective_apply, liftQ_mkQ, ker_liftQ, LinearMap.ker_eq_bot_range_liftQ_iff, comap_liftQ, range_liftQ
liftQSpanSingleton 📖	CompOp	1 math math: liftQSpanSingleton_apply
mapQ 📖	CompOp	17 math math: Module.End.IsNilpotent.mapQ, mapQ_apply, quotientQuotientEquivQuotientAux_mk, mapQ_pow, Function.Exact.exact_mapQ_iff, mapQ_zero, mapQ_eq_factor, quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, Quotient.equiv_symm_apply, piQuotientLift_single, mapQ_mkQ, Representation.quotient_apply, LinearMap.det_eq_det_mul_det, RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last, mapQ_comp, mapQ_id, Quotient.equiv_apply
mapQLinear 📖	CompOp	—
quotEquivOfEqBot 📖	CompOp	3 math math: quotEquivOfEqBot_symm_apply, coe_quotEquivOfEqBot_symm, quotEquivOfEqBot_apply_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_quotEquivOfEqBot_symm 📖	mathematical	Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instBot	LinearEquiv.toLinearMap RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module LinearEquiv.symm quotEquivOfEqBot mkQ	—	RingHomInvPair.ids
comapMkQOrderEmbedding_eq 📖	mathematical	—	DFunLike.coe OrderEmbedding Submodule HasQuotient.Quotient Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module Preorder.toLE PartialOrder.toPreorder instPartialOrder instFunLikeOrderEmbedding comapMkQOrderEmbedding comap RingHom.id Semiring.toNonAssocSemiring mkQ	—	—
comap_liftQ 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker	comap HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module liftQ map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mkQ	—	le_antisymm RingHomSurjective.ids map_le_iff_le_comap RingHomCompTriple.ids comap_comp liftQ_mkQ le_refl
comap_map_mkQ 📖	mathematical	—	comap HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring mkQ map RingHomSurjective.ids SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	RingHomSurjective.ids comap_map_eq ker_mkQ sup_comm
factor_comp 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	LinearMap.comp HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids factor LE.le.trans	—	linearMap_qext RingHomCompTriple.ids LE.le.trans LinearMap.ext
factor_comp_apply 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module LinearMap.instFunLike factor LE.le.trans	—	LE.le.trans RingHomCompTriple.ids LinearMap.comp_apply factor_comp
factor_comp_mk 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	LinearMap.comp HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids factor mkQ	—	LinearMap.ext RingHomCompTriple.ids LinearMap.comp_apply
factor_mk 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module LinearMap.instFunLike factor mkQ	—	—
factor_surjective 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	HasQuotient.Quotient hasQuotient DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Quotient.addCommGroup Quotient.module LinearMap.instFunLike factor	—	Quotient.out_eq
ker_liftQ 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker	HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module liftQ map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mkQ	—	comap_liftQ
ker_liftQ_eq_bot 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker	HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module liftQ Bot.bot instBot	—	RingHomSurjective.ids ker_liftQ le_antisymm mkQ_map_self
ker_liftQ_eq_bot' 📖	mathematical	LinearMap.ker Ring.toSemiring AddCommGroup.toAddCommMonoid	HasQuotient.Quotient Submodule hasQuotient Quotient.addCommGroup Quotient.module liftQ le_of_eq PartialOrder.toPreorder instPartialOrder Bot.bot instBot	—	ker_liftQ_eq_bot Eq.le Eq.ge
ker_mkQ 📖	mathematical	—	LinearMap.ker HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring mkQ	—	ext
le_comap_mkQ 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring mkQ	—	ker_mkQ comap_mono bot_le
liftQSpanSingleton_apply 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring AddCommGroup.toAddCommMonoid LinearMap.instFunLike NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	HasQuotient.Quotient Submodule hasQuotient span Set Set.instSingletonSet Quotient.addCommGroup Quotient.module liftQSpanSingleton	—	—
liftQ_apply 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker	DFunLike.coe LinearMap HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module LinearMap.instFunLike liftQ	—	—
liftQ_mkQ 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker	LinearMap.comp HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids liftQ mkQ	—	LinearMap.ext RingHomCompTriple.ids
mapQ_apply 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap	DFunLike.coe LinearMap HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module LinearMap.instFunLike mapQ	—	—
mapQ_comp 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap LE.le.trans comap_mono	mapQ LinearMap.comp HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module	—	linearMap_qext LinearMap.ext RingHomCompTriple.ids
mapQ_id 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap RingHom.id Semiring.toNonAssocSemiring LinearMap.id	mapQ HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module	—	linearMap_qext LinearMap.ext RingHomCompTriple.ids
mapQ_mkQ 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap	LinearMap.comp HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomCompTriple.ids mapQ mkQ RingHomCompTriple.right_ids	—	LinearMap.ext RingHomCompTriple.ids RingHomCompTriple.right_ids
mapQ_pow 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap RingHom.id Semiring.toNonAssocSemiring LinearMap Monoid.toNatPow Module.End.instMonoid le_comap_pow_of_le_comap	mapQ HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module	—	pow_zero mapQ.congr_simp mapQ_id RingHomCompTriple.ids Module.End.iterate_succ le_comap_pow_of_le_comap LE.le.trans comap_mono mapQ_comp
mapQ_zero 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder comap LinearMap LinearMap.instZero	mapQ HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module	—	linearMap_qext LinearMap.ext RingHomCompTriple.ids
map_liftQ 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker	map HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module liftQ comap RingHom.id Semiring.toNonAssocSemiring mkQ	—	le_antisymm
map_mkQ_eq_top 📖	mathematical	—	map HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mkQ Top.top instTop SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	RingHomSurjective.ids LinearMap.map_eq_top_iff range_mkQ ker_mkQ sup_comm
mkQ_map_self 📖	mathematical	—	map HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mkQ Bot.bot instBot	—	RingHomSurjective.ids eq_bot_iff map_le_iff_le_comap comap_bot ker_mkQ le_refl
pi_liftQ_eq_liftQ_pi 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker RingHom.id Semiring.toNonAssocSemiring	LinearMap.pi HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module liftQ Pi.addCommGroup Pi.module iInf instInfSet le_iInf completeLattice Pi.addCommMonoid LinearMap.ker_pi	—	linearMap_qext le_iInf LinearMap.ker_pi LinearMap.ext RingHomCompTriple.ids liftQ_mkQ
quotEquivOfEqBot_apply_mk 📖	mathematical	Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instBot	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike quotEquivOfEqBot	—	RingHomInvPair.ids
quotEquivOfEqBot_symm_apply 📖	mathematical	Bot.bot Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instBot	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotEquivOfEqBot	—	RingHomInvPair.ids
range_liftQ 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder LinearMap.ker	LinearMap.range HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module liftQ	—	LinearMap.range_eq_map map_liftQ
range_mkQ 📖	mathematical	—	LinearMap.range HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Quotient.addCommGroup Quotient.module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mkQ Top.top instTop	—	RingHomSurjective.ids eq_top_iff'
span_preimage_eq 📖	mathematical	Set.Nonempty Set Set.instHasSubset SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid setLike LinearMap.range	span Set.preimage DFunLike.coe LinearMap LinearMap.instFunLike comap	—	LinearMap.ker_le_iff Set.Subset.trans subset_span span_mono Set.preimage_mono Set.singleton_subset_iff left_eq_sup LinearMap.map_le_map_iff map_span map_comap_eq Set.image_preimage_eq_of_subset LinearMap.coe_range inf_le_right le_antisymm span_preimage_le
strictMono_comap_prod_map 📖	mathematical	—	StrictMono Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike addCommMonoid module HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module PartialOrder.toPreorder instPartialOrder Prod.instPreorder comap RingHom.id Semiring.toNonAssocSemiring subtype map RingHomSurjective.ids mkQ	—	QuotientAddGroup.strictMono_comap_prod_map AddSubgroup.normal_of_comm
subsingleton_quotient_iff_eq_top 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Top.top instTop	—	Quotient.subsingleton_iff
unique_quotient_iff_eq_top 📖	mathematical	—	Unique HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid hasQuotient Top.top instTop	—	Quotient.subsingleton_iff Unique.instSubsingleton

Submodule.Quotient

Definitions

Name	Category	Theorems
equiv 📖	CompOp	5 math math: equiv_symm, equiv_symm_apply, equiv_refl, equiv_trans, equiv_apply
fintype 📖	CompOp	—
restrictScalarsEquiv 📖	CompOp	2 math math: restrictScalarsEquiv_symm_mk, restrictScalarsEquiv_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
equiv_apply 📖	mathematical	Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids	DFunLike.coe LinearEquiv HasQuotient.Quotient Submodule Submodule.hasQuotient addCommGroup module EquivLike.toFunLike LinearEquiv.instEquivLike equiv LinearMap LinearMap.instFunLike Submodule.mapQ	—	RingHomInvPair.ids RingHomSurjective.ids
equiv_refl 📖	mathematical	Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.refl	equiv Submodule.quotEquivOfEq	—	RingHomSurjective.ids RingHomInvPair.ids
equiv_symm 📖	mathematical	Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids	LinearEquiv.symm HasQuotient.Quotient Submodule Submodule.hasQuotient addCommGroup module equiv RingHomSurjective.invPair Submodule.map_symm_eq_iff	—	RingHomInvPair.ids RingHomSurjective.ids
equiv_symm_apply 📖	mathematical	Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids	DFunLike.coe LinearEquiv HasQuotient.Quotient Submodule Submodule.hasQuotient addCommGroup module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm equiv LinearMap LinearMap.instFunLike Submodule.mapQ	—	RingHomInvPair.ids RingHomSurjective.ids
equiv_trans 📖	mathematical	Submodule.map Ring.toSemiring AddCommGroup.toAddCommMonoid RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.trans RingHomCompTriple.ids	equiv HasQuotient.Quotient Submodule Submodule.hasQuotient addCommGroup module	—	RingHomInvPair.ids RingHomSurjective.ids RingHomCompTriple.ids LinearEquiv.ext LE.le.trans Submodule.comap_mono Submodule.mapQ_comp LinearMap.comp_apply
instSubsingletonQuotient 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient	—	Unique.instSubsingleton
nontrivial_iff 📖	mathematical	—	Nontrivial HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient	—	QuotientAddGroup.nontrivial_iff
nontrivial_of_lt_top 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLT PartialOrder.toPreorder Submodule.instPartialOrder Top.top Submodule.instTop	Nontrivial HasQuotient.Quotient Submodule.hasQuotient	—	nontrivial_iff LT.lt.ne
nontrivial_of_ne_top 📖	mathematical	—	Nontrivial HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient	—	nontrivial_iff
restrictScalarsEquiv_mk 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.restrictScalars addCommGroup module module' EquivLike.toFunLike LinearEquiv.instEquivLike restrictScalarsEquiv	—	RingHomInvPair.ids
restrictScalarsEquiv_symm_mk 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid Submodule.hasQuotient Submodule.restrictScalars addCommGroup module' module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm restrictScalarsEquiv	—	RingHomInvPair.ids
subsingleton_iff 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient Top.top Submodule.instTop	—	QuotientAddGroup.subsingleton_iff

Submodule.QuotientBot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
infinite 📖	mathematical	—	Infinite HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Submodule.hasQuotient Bot.bot Submodule.instBot	—	Infinite.of_injective sub_eq_zero Submodule.Quotient.eq

Submodule.QuotientTop

Definitions

Name	Category	Theorems
fintype 📖	CompOp	—
unique 📖	CompOp	—

---

← Back to Index