Isomorphisms

📁 Source: Mathlib/LinearAlgebra/Isomorphisms.lean

Statistics

Metric	Count
Definitions quotKerEquivOfSurjective, quotKerEquivRange, quotientInfEquivSupQuotient, quotientInfToSupQuotient, subToSupQuotient, quotientQuotientEquivQuotient, quotientQuotientEquivQuotientAux, quotientQuotientEquivQuotientSup	8
Theorems coe_quotientInfToSupQuotient, comap_leq_ker_subToSupQuotient, quotKerEquivOfSurjective_apply_mk, quotKerEquivOfSurjective_symm_apply, quotKerEquivRange_apply_mk, quotKerEquivRange_symm_apply_image, quotientInfEquivSupQuotient_apply_mk, quotientInfEquivSupQuotient_injective, quotientInfEquivSupQuotient_surjective, quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, quotientInfEquivSupQuotient_symm_apply_left, quotientInfEquivSupQuotient_symm_apply_right, card_quotient_mul_card_quotient, quotientQuotientEquivQuotientAux_mk, quotientQuotientEquivQuotientAux_mk_mk	15
Total	23

LinearMap

Definitions

Name	Category	Theorems
quotKerEquivOfSurjective 📖	CompOp	2 math math: quotKerEquivOfSurjective_symm_apply, quotKerEquivOfSurjective_apply_mk
quotKerEquivRange 📖	CompOp	6 math math: LieHom.quotKerEquivRange_toFun, CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe, CharacterModule.intSpanEquivQuotAddOrderOf_apply, quotKerEquivRange_symm_apply_image, quotKerEquivRange_apply_mk, LieHom.quotKerEquivRange_invFun
quotientInfEquivSupQuotient 📖	CompOp	5 math math: quotientInfEquivSupQuotient_symm_apply_eq_zero_iff, quotientInfEquivSupQuotient_apply_mk, coe_quotientInfToSupQuotient, quotientInfEquivSupQuotient_symm_apply_left, quotientInfEquivSupQuotient_symm_apply_right
quotientInfToSupQuotient 📖	CompOp	3 math math: quotientInfEquivSupQuotient_injective, coe_quotientInfToSupQuotient, quotientInfEquivSupQuotient_surjective
subToSupQuotient 📖	CompOp	1 math math: comap_leq_ker_subToSupQuotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_quotientInfToSupQuotient 📖	mathematical	—	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup Submodule.instMin Submodule.comap Submodule.subtype SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.Quotient.addCommGroup Submodule.Quotient.module instFunLike quotientInfToSupQuotient LinearEquiv RingHomInvPair.ids EquivLike.toFunLike LinearEquiv.instEquivLike quotientInfEquivSupQuotient	—	—
comap_leq_ker_subToSupQuotient 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder Submodule.comap RingHom.id Semiring.toNonAssocSemiring Submodule.subtype Submodule.instMin ker HasQuotient.Quotient SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.hasQuotient Submodule.addCommGroup Submodule.Quotient.addCommGroup Submodule.Quotient.module subToSupQuotient	—	ker_comp Submodule.inclusion.eq_1 RingHomSurjective.ids comap_codRestrict Submodule.ker_mkQ Submodule.map_comap_subtype Submodule.comap_mono inf_le_inf_right le_sup_left
quotKerEquivOfSurjective_apply_mk 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	LinearEquiv RingHomInvPair.ids HasQuotient.Quotient Submodule Submodule.hasQuotient ker Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike quotKerEquivOfSurjective	—	RingHomInvPair.ids
quotKerEquivOfSurjective_symm_apply 📖	mathematical	DFunLike.coe LinearMap Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring AddCommGroup.toAddCommMonoid instFunLike	LinearEquiv RingHomInvPair.ids HasQuotient.Quotient Submodule Submodule.hasQuotient ker Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotKerEquivOfSurjective	—	RingHomInvPair.ids
quotKerEquivRange_apply_mk 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearEquiv RingHomInvPair.ids HasQuotient.Quotient Submodule.hasQuotient ker Submodule.Quotient.addCommGroup Submodule.addCommMonoid Submodule.Quotient.module Submodule.module EquivLike.toFunLike LinearEquiv.instEquivLike quotKerEquivRange LinearMap instFunLike	—	RingHomSurjective.ids RingHomInvPair.ids
quotKerEquivRange_symm_apply_image 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike range RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids DFunLike.coe LinearMap instFunLike	LinearEquiv RingHomInvPair.ids HasQuotient.Quotient Submodule.hasQuotient ker Submodule.addCommMonoid Submodule.Quotient.addCommGroup Submodule.module Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotKerEquivRange Submodule.mkQ	—	RingHomSurjective.ids LinearEquiv.symm_apply_apply RingHomInvPair.ids
quotientInfEquivSupQuotient_apply_mk 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup Submodule.instMin Submodule.comap Submodule.subtype SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike quotientInfEquivSupQuotient LinearMap instFunLike Submodule.inclusion le_sup_left	—	RingHomInvPair.ids
quotientInfEquivSupQuotient_injective 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup Submodule.instMin Submodule.comap RingHom.id Semiring.toNonAssocSemiring Submodule.subtype SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice DFunLike.coe LinearMap Submodule.Quotient.addCommGroup Submodule.Quotient.module instFunLike quotientInfToSupQuotient	—	ker_eq_bot comap_leq_ker_subToSupQuotient quotientInfToSupQuotient.eq_1 Submodule.ker_liftQ_eq_bot ker_comp Submodule.ker_mkQ
quotientInfEquivSupQuotient_surjective 📖	mathematical	—	HasQuotient.Quotient Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup Submodule.instMin Submodule.comap RingHom.id Semiring.toNonAssocSemiring Submodule.subtype SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice DFunLike.coe LinearMap Submodule.Quotient.addCommGroup Submodule.Quotient.module instFunLike quotientInfToSupQuotient	—	RingHomSurjective.ids range_eq_top comap_leq_ker_subToSupQuotient quotientInfToSupQuotient.eq_1 Submodule.range_liftQ Submodule.eq_top_iff' Submodule.mem_sup Submodule.Quotient.eq map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass semilinearMapClass sub_add_cancel_left AddSubgroupClass.toNegMemClass Submodule.addSubgroupClass
quotientInfEquivSupQuotient_symm_apply_eq_zero_iff 📖	mathematical	—	DFunLike.coe LinearEquiv Ring.toSemiring RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup Submodule.comap Submodule.subtype Submodule.instMin Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotientInfEquivSupQuotient Submodule.Quotient.instZeroQuotient	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass
quotientInfEquivSupQuotient_symm_apply_left 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup Submodule.comap Submodule.subtype Submodule.instMin Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotientInfEquivSupQuotient	—	RingHomInvPair.ids LinearEquiv.symm_apply_eq le_sup_left Submodule.inclusion_apply
quotientInfEquivSupQuotient_symm_apply_right 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership Submodule.setLike SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids HasQuotient.Quotient Submodule.addCommMonoid Submodule.module Submodule.hasQuotient Submodule.addCommGroup Submodule.comap Submodule.subtype Submodule.instMin Submodule.Quotient.addCommGroup Submodule.Quotient.module EquivLike.toFunLike LinearEquiv.instEquivLike LinearEquiv.symm quotientInfEquivSupQuotient Submodule.Quotient.instZeroQuotient	—	RingHomInvPair.ids quotientInfEquivSupQuotient_symm_apply_eq_zero_iff

Submodule

Definitions

Name	Category	Theorems
quotientQuotientEquivQuotient 📖	CompOp	—
quotientQuotientEquivQuotientAux 📖	CompOp	2 math math: quotientQuotientEquivQuotientAux_mk, quotientQuotientEquivQuotientAux_mk_mk
quotientQuotientEquivQuotientSup 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_quotient_mul_card_quotient 📖	mathematical	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder	Nat.card HasQuotient.Quotient hasQuotient Quotient.addCommGroup Quotient.module SetLike.instMembership setLike map RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids mkQ	—	RingHomSurjective.ids card_eq_card_quotient_mul_card Nat.card_congr RingHomInvPair.ids
quotientQuotientEquivQuotientAux_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 map RingHomSurjective.ids mkQ LinearMap.instFunLike quotientQuotientEquivQuotientAux mapQ LinearMap.id	—	liftQ_apply
quotientQuotientEquivQuotientAux_mk_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 map RingHomSurjective.ids mkQ LinearMap.instFunLike quotientQuotientEquivQuotientAux	—	RingHomSurjective.ids

---

← Back to Index