Hom

📁 Source: Mathlib/RingTheory/Congruence/Hom.lean

Statistics

Metric	Count
Definitions `comapQuotientEquivOfSurj`, `comapQuotientEquivRange`, `comapQuotientEquivRangeS`, `comapQuotientEquivRangeₐ`, `congrₐ`, `correspondence`, `factorₐ`, `ker`, `kerLift`, `kerLiftₐ`, `liftₐ`, `map`, `mapGen`, `quotientKerEquivOfRightInverse`, `quotientKerEquivOfSurjective`, `quotientKerEquivRange`, `quotientKerEquivRangeS`, `quotientKerEquivRangeₐ`, `quotientQuotientEquivQuotient`, `quotientQuotientEquivQuotientₐ`	20
Theorems `hom_ext`, `hom_ext_iff`, `coe_comapQuotientEquivRange_mk`, `coe_comapQuotientEquivRangeₐ_mk`, `coe_comapQuotientEquivRangeₐ_symm_mk`, `coe_liftₐ`, `coe_quotientKerEquivRangeS_mk`, `coe_quotientKerEquivRangeₐ_mkₐ`, `comapQuotientEquivOfSurj_mk`, `comapQuotientEquivOfSurj_symm_mk`, `comapQuotientEquivOfSurj_symm_mk'`, `comapQuotientEquivRangeS_mk`, `comapQuotientEquivRangeS_symm_mk`, `comapQuotientEquivRange_mk`, `comapQuotientEquivRange_symm_mk`, `comapQuotientEquivRangeₐ_mk`, `comap_bot`, `comap_eq`, `congr_mk`, `congrₐ_mk`, `factorₐ_apply`, `factorₐ_mk`, `kerLift_injective`, `kerLift_mk`, `kerLift_range_eq`, `kerLiftₐ_injective`, `kerLiftₐ_mk`, `kerLiftₐ_range_eq`, `ker_apply`, `ker_comp`, `ker_eq_lift_of_injective`, `ker_mk'_eq`, `lift_apply_mk'`, `lift_bijective_iff`, `lift_coe`, `lift_comp_mk'`, `lift_injective_iff`, `lift_mk'`, `lift_surjective_iff`, `lift_surjective_of_surjective`, `lift_unique`, `liftₐ_coe_toRingHom`, `liftₐ_mk`, `liftₐ_range`, `mapGen_apply_apply_of_surjective`, `mapGen_eq_map_of_surjective`, `map_apply`, `mkₐ_comp_factorₐ_comp_mkₐ`, `quotientKerEquivOfRightInverse_apply`, `quotientKerEquivOfSurjective_mk`, `quotientKerEquivRangeₐ_comp_mkₐ`, `quotientKerEquivRangeₐ_mkₐ`, `quotientQuotientEquivQuotient_coe_coe`, `quotientQuotientEquivQuotient_mk_mk`, `quotientQuotientEquivQuotient_symm_mk`, `quotientQuotientEquivQuotientₐ_coe_coe`, `quotientQuotientEquivQuotientₐ_mk_mk`, `quotientQuotientEquivQuotientₐ_symm_mk`, `rangeS_kerLift`, `rangeS_lift`, `rangeS_mk'`, `range_lift`, `range_mk'`, `range_mkₐ`	64
Total	84

RingCon

Definitions

Name	Category	Theorems
`comapQuotientEquivOfSurj` 📖	CompOp	3 math math: `comapQuotientEquivOfSurj_symm_mk`, `comapQuotientEquivOfSurj_symm_mk'`, `comapQuotientEquivOfSurj_mk`
`comapQuotientEquivRange` 📖	CompOp	3 math math: `comapQuotientEquivRange_symm_mk`, `comapQuotientEquivRange_mk`, `coe_comapQuotientEquivRange_mk`
`comapQuotientEquivRangeS` 📖	CompOp	2 math math: `comapQuotientEquivRangeS_symm_mk`, `comapQuotientEquivRangeS_mk`
`comapQuotientEquivRangeₐ` 📖	CompOp	3 math math: `coe_comapQuotientEquivRangeₐ_mk`, `coe_comapQuotientEquivRangeₐ_symm_mk`, `comapQuotientEquivRangeₐ_mk`
`congrₐ` 📖	CompOp	1 math math: `congrₐ_mk`
`correspondence` 📖	CompOp	—
`factorₐ` 📖	CompOp	6 math math: `mkₐ_comp_factorₐ_comp_mkₐ`, `factorₐ_mk`, `quotientQuotientEquivQuotientₐ_mk_mk`, `factorₐ_apply`, `quotientQuotientEquivQuotientₐ_symm_mk`, `quotientQuotientEquivQuotientₐ_coe_coe`
`ker` 📖	CompOp	24 math math: `ker_apply`, `comap_bot`, `rangeS_kerLift`, `quotientKerEquivRangeₐ_comp_mkₐ`, `ker_comp`, `kerLiftₐ_mk`, `quotientQuotientEquivQuotient_coe_coe`, `quotientKerEquivOfRightInverse_apply`, `coe_quotientKerEquivRangeS_mk`, `kerLiftₐ_injective`, `kerLift_range_eq`, `kerLiftₐ_range_eq`, `quotientQuotientEquivQuotientₐ_mk_mk`, `quotientQuotientEquivQuotient_mk_mk`, `quotientQuotientEquivQuotientₐ_symm_mk`, `kerLift_injective`, `ker_mk'_eq`, `quotientKerEquivRangeₐ_mkₐ`, `kerLift_mk`, `quotientQuotientEquivQuotient_symm_mk`, `quotientKerEquivOfSurjective_mk`, `quotientQuotientEquivQuotientₐ_coe_coe`, `comap_eq`, `coe_quotientKerEquivRangeₐ_mkₐ`
`kerLift` 📖	CompOp	5 math math: `rangeS_kerLift`, `quotientKerEquivOfRightInverse_apply`, `kerLift_range_eq`, `kerLift_injective`, `kerLift_mk`
`kerLiftₐ` 📖	CompOp	3 math math: `kerLiftₐ_mk`, `kerLiftₐ_injective`, `kerLiftₐ_range_eq`
`liftₐ` 📖	CompOp	5 math math: `factorₐ_apply`, `liftₐ_range`, `liftₐ_mk`, `coe_liftₐ`, `liftₐ_coe_toRingHom`
`map` 📖	CompOp	4 math math: `quotientQuotientEquivQuotient_coe_coe`, `quotientQuotientEquivQuotient_mk_mk`, `quotientQuotientEquivQuotient_symm_mk`, `map_apply`
`mapGen` 📖	CompOp	2 math math: `mapGen_apply_apply_of_surjective`, `mapGen_eq_map_of_surjective`
`quotientKerEquivOfRightInverse` 📖	CompOp	1 math math: `quotientKerEquivOfRightInverse_apply`
`quotientKerEquivOfSurjective` 📖	CompOp	1 math math: `quotientKerEquivOfSurjective_mk`
`quotientKerEquivRange` 📖	CompOp	—
`quotientKerEquivRangeS` 📖	CompOp	1 math math: `coe_quotientKerEquivRangeS_mk`
`quotientKerEquivRangeₐ` 📖	CompOp	3 math math: `quotientKerEquivRangeₐ_comp_mkₐ`, `quotientKerEquivRangeₐ_mkₐ`, `coe_quotientKerEquivRangeₐ_mkₐ`
`quotientQuotientEquivQuotient` 📖	CompOp	3 math math: `quotientQuotientEquivQuotient_coe_coe`, `quotientQuotientEquivQuotient_mk_mk`, `quotientQuotientEquivQuotient_symm_mk`
`quotientQuotientEquivQuotientₐ` 📖	CompOp	3 math math: `quotientQuotientEquivQuotientₐ_mk_mk`, `quotientQuotientEquivQuotientₐ_symm_mk`, `quotientQuotientEquivQuotientₐ_coe_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_comapQuotientEquivRange_mk` 📖	mathematical	`comap` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `RingHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHomClass.toNonUnitalRingHomClass`	`Quotient` `Subring` `instRingQuotient` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `RingHom.comp` `instNonAssocSemiringQuotient` `mk'` `DFunLike.coe` `RingEquiv` `instMulQuotient` `Subring.toRing` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `comapQuotientEquivRange` `toQuotient`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`coe_comapQuotientEquivRangeₐ_mk` 📖	mathematical	`comap` `AlgHom` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AlgHom.funLike` `SemilinearMapClass.toAddHomClass` `CommSemiring.toSemiring` `RingHom.id` `Algebra.toModule` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Distrib.toMul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Module.toDistribMulAction`	`Quotient` `Subalgebra` `instSemiringQuotient` `instAlgebraQuotient` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `AlgHom.comp` `mkₐ` `DFunLike.coe` `AlgEquiv` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgEquiv.instFunLike` `comapQuotientEquivRangeₐ` `toQuotient`	—	`SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `NonUnitalAlgSemiHomClass.toMulHomClass`
`coe_comapQuotientEquivRangeₐ_symm_mk` 📖	mathematical	`comap` `AlgHom` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AlgHom.funLike` `SemilinearMapClass.toAddHomClass` `CommSemiring.toSemiring` `RingHom.id` `Algebra.toModule` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Distrib.toMul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Module.toDistribMulAction`	`DFunLike.coe` `AlgEquiv` `Quotient` `Subalgebra` `instSemiringQuotient` `instAlgebraQuotient` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `AlgHom.comp` `mkₐ` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgEquiv.instFunLike` `AlgEquiv.symm` `comapQuotientEquivRangeₐ` `toQuotient` `AlgHom.mem_range_self`	—	`SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `NonUnitalAlgSemiHomClass.toMulHomClass` `AlgHom.mem_range_self`
`coe_liftₐ` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `AlgHom.toRingHom`	`DFunLike.coe` `AlgHom` `Quotient` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `liftₐ` `RingHom` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `lift` `RingHomClass.toRingHom` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`	—	—
`coe_quotientKerEquivRangeS_mk` 📖	mathematical	—	`Subsemiring` `SetLike.instMembership` `Subsemiring.instSetLike` `RingHom.rangeS` `DFunLike.coe` `RingEquiv` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `ker` `instMulQuotient` `Subsemiring.toNonAssocSemiring` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `quotientKerEquivRangeS` `toQuotient` `RingHom` `RingHom.instFunLike`	—	—
`coe_quotientKerEquivRangeₐ_mkₐ` 📖	mathematical	—	`Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `DFunLike.coe` `AlgEquiv` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `ker` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `instSemiringQuotient` `Subalgebra.toSemiring` `instAlgebraQuotient` `Subalgebra.algebra` `AlgEquiv.instFunLike` `quotientKerEquivRangeₐ` `toQuotient`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`comapQuotientEquivOfSurj_mk` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike` `comap` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`	`RingEquiv` `Quotient` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `comapQuotientEquivOfSurj` `toQuotient`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`comapQuotientEquivOfSurj_symm_mk` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike` `comap` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`	`RingEquiv` `Quotient` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `comapQuotientEquivOfSurj` `toQuotient`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingEquiv.symm_apply_apply`
`comapQuotientEquivOfSurj_symm_mk'` 📖	mathematical	`comap` `RingEquiv` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass`	`DFunLike.coe` `Quotient` `instMulQuotient` `instAddQuotient` `RingEquiv.symm` `comapQuotientEquivOfSurj` `RingHomClass.toRingHom` `RingEquiv.surjective` `Con.toSetoid` `toCon` `toQuotient`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingEquivClass.toRingHomClass` `RingEquiv.instRingEquivClass` `NonUnitalRingHomClass.toMulHomClass` `RingEquivClass.toNonUnitalRingHomClass` `RingEquiv.surjective` `RingEquiv.coe_toRingHom` `RingEquiv.symm_apply_apply`
`comapQuotientEquivRangeS_mk` 📖	mathematical	`comap` `RingHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`	`DFunLike.coe` `RingEquiv` `Quotient` `Subsemiring` `instNonAssocSemiringQuotient` `SetLike.instMembership` `Subsemiring.instSetLike` `RingHom.rangeS` `RingHom.comp` `mk'` `instMulQuotient` `Subsemiring.toNonAssocSemiring` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `comapQuotientEquivRangeS` `toQuotient` `RingHom.mem_rangeS_self`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`comapQuotientEquivRangeS_symm_mk` 📖	mathematical	`comap` `RingHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`	`DFunLike.coe` `RingEquiv` `Quotient` `Subsemiring` `instNonAssocSemiringQuotient` `SetLike.instMembership` `Subsemiring.instSetLike` `RingHom.rangeS` `RingHom.comp` `mk'` `Subsemiring.toNonAssocSemiring` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `comapQuotientEquivRangeS` `toQuotient` `RingHom.mem_rangeS_self`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.mem_rangeS_self`
`comapQuotientEquivRange_mk` 📖	mathematical	`comap` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `RingHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHomClass.toNonUnitalRingHomClass`	`DFunLike.coe` `RingEquiv` `Quotient` `Subring` `instRingQuotient` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `RingHom.comp` `instNonAssocSemiringQuotient` `mk'` `instMulQuotient` `Subring.toRing` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `comapQuotientEquivRange` `toQuotient` `RingHom.mem_range_self`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`comapQuotientEquivRange_symm_mk` 📖	mathematical	`comap` `RingHom` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `RingHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHomClass.toNonUnitalRingHomClass`	`DFunLike.coe` `RingEquiv` `Quotient` `Subring` `instRingQuotient` `SetLike.instMembership` `Subring.instSetLike` `RingHom.range` `RingHom.comp` `instNonAssocSemiringQuotient` `mk'` `Subring.toRing` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `comapQuotientEquivRange` `toQuotient` `RingHom.mem_range_self`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `RingHom.mem_range_self`
`comapQuotientEquivRangeₐ_mk` 📖	mathematical	`comap` `AlgHom` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `AddCommMonoid.toAddCommSemigroup` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `AlgHom.funLike` `SemilinearMapClass.toAddHomClass` `CommSemiring.toSemiring` `RingHom.id` `Algebra.toModule` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `Distrib.toMul` `NonUnitalAlgSemiHomClass.toMulHomClass` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `MonoidHom.id` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Module.toDistribMulAction`	`DFunLike.coe` `AlgEquiv` `Quotient` `Subalgebra` `instSemiringQuotient` `instAlgebraQuotient` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `AlgHom.comp` `mkₐ` `Subalgebra.toSemiring` `Subalgebra.algebra` `AlgEquiv.instFunLike` `comapQuotientEquivRangeₐ` `toQuotient` `AlgHom.mem_range_self`	—	`SemilinearMapClass.toAddHomClass` `NonUnitalAlgHomClass.instLinearMapClass` `AlgHom.instNonUnitalAlgHomClassOfAlgHomClass` `AlgHom.algHomClass` `NonUnitalAlgSemiHomClass.toMulHomClass`
`comap_bot` 📖	mathematical	—	`comap` `RingHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `Bot.bot` `RingCon` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `ker`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`comap_eq` 📖	mathematical	—	`comap` `RingHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `ker` `Quotient` `instNonAssocSemiringQuotient` `RingHom.comp` `mk'`	—	`AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `ker_comp` `ker_mk'_eq`
`congr_mk` 📖	mathematical	—	`DFunLike.coe` `RingEquiv` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `congr` `toQuotient`	—	—
`congrₐ_mk` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instSemiringQuotient` `instAlgebraQuotient` `AlgEquiv.instFunLike` `congrₐ` `toQuotient`	—	—
`factorₐ_apply` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `AlgHom` `Quotient` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `factorₐ` `liftₐ` `mkₐ` `toQuotient` `instFunLikeForallProp` `eq`	—	—
`factorₐ_mk` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `AlgHom` `Quotient` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `factorₐ` `Con.toSetoid` `toCon`	—	—
`kerLift_injective` 📖	mathematical	—	`Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `ker` `DFunLike.coe` `RingHom` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `kerLift`	—	`AddCon.kerLift_injective` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass`
`kerLift_mk` 📖	mathematical	—	`DFunLike.coe` `RingHom` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `ker` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `kerLift` `toQuotient`	—	—
`kerLift_range_eq` 📖	mathematical	—	`RingHom.range` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Distrib.toMul` `ker` `instRingQuotient` `kerLift`	—	`range_lift`
`kerLiftₐ_injective` 📖	mathematical	—	`Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `ker` `AlgHom.toRingHom` `DFunLike.coe` `AlgHom` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `kerLiftₐ`	—	`kerLift_injective`
`kerLiftₐ_mk` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `ker` `AlgHom.toRingHom` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `kerLiftₐ` `toQuotient`	—	—
`kerLiftₐ_range_eq` 📖	mathematical	—	`AlgHom.range` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `ker` `AlgHom.toRingHom` `instSemiringQuotient` `instAlgebraQuotient` `kerLiftₐ`	—	`liftₐ_range`
`ker_apply` 📖	mathematical	—	`DFunLike.coe` `RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instFunLikeForallProp` `ker` `RingHom` `RingHom.instFunLike`	—	—
`ker_comp` 📖	mathematical	—	`ker` `RingHom.comp` `comap` `RingHom` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddMonoidWithOne.toAddMonoid` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `RingHom.instFunLike` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `Distrib.toMul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`	—	`ext` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass`
`ker_eq_lift_of_injective` 📖	—	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `Quotient` `DFunLike.coe` `RingHom` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `lift`	—	—	`lift_injective_iff`
`ker_mk'_eq` 📖	mathematical	—	`ker` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instNonAssocSemiringQuotient` `mk'`	—	`ext` `Quotient.eq''`
`lift_apply_mk'` 📖	mathematical	—	`lift` `RingHom.comp` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instNonAssocSemiringQuotient` `mk'`	—	`RingHom.ext`
`lift_bijective_iff` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker`	`Function.Bijective` `Quotient` `DFunLike.coe` `RingHom` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `lift`	—	—
`lift_coe` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker`	`DFunLike.coe` `RingHom` `Quotient` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `lift` `toQuotient`	—	—
`lift_comp_mk'` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker`	`RingHom.comp` `Quotient` `instNonAssocSemiringQuotient` `lift` `mk'`	—	—
`lift_injective_iff` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker`	`Quotient` `DFunLike.coe` `RingHom` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `lift`	—	`ext''` `Setoid.ker_eq_lift_of_injective`
`lift_mk'` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker`	`DFunLike.coe` `RingHom` `Quotient` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `lift` `mk'`	—	—
`lift_surjective_iff` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker`	`Quotient` `DFunLike.coe` `RingHom` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `lift`	—	`Quot.surjective_lift` `AddCon.lift_surjective_of_surjective`
`lift_surjective_of_surjective` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	`Quotient` `instNonAssocSemiringQuotient` `lift`	—	`lift_surjective_iff`
`lift_unique` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `RingHom.comp` `Quotient` `instNonAssocSemiringQuotient` `mk'`	`lift`	—	`Quotient.hom_ext`
`liftₐ_coe_toRingHom` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `AlgHom.toRingHom`	`Quotient` `instSemiringQuotient` `instAlgebraQuotient` `liftₐ` `lift` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass`	—	—
`liftₐ_mk` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `AlgHom.toRingHom`	`DFunLike.coe` `AlgHom` `Quotient` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `liftₐ` `toQuotient`	—	—
`liftₐ_range` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `AlgHom.toRingHom`	`AlgHom.range` `Quotient` `instSemiringQuotient` `instAlgebraQuotient` `liftₐ`	—	`Subalgebra.toSubsemiring_injective` `rangeS_lift`
`mapGen_apply_apply_of_surjective` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	`instFunLikeForallProp` `mapGen`	—	`mapGen_eq_map_of_surjective` `Relation.map_apply` `trans`
`mapGen_eq_map_of_surjective` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker` `DFunLike.coe` `RingHom` `RingHom.instFunLike`	`instFunLikeForallProp` `mapGen` `Relation.Map`	—	`le_antisymm` `Relation.map_equivalence` `add` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `RingHom.instRingHomClass` `mul` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `GaloisConnection.le_u_l` `GaloisInsertion.gc`
`map_apply` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `RingHom` `Quotient` `instNonAssocSemiringQuotient` `RingHom.instFunLike` `map` `lift` `mk'` `toQuotient` `instFunLikeForallProp` `eq`	—	—
`mkₐ_comp_factorₐ_comp_mkₐ` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE`	`AlgHom.comp` `Quotient` `instSemiringQuotient` `instAlgebraQuotient` `factorₐ` `mkₐ`	—	—
`quotientKerEquivOfRightInverse_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`RingEquiv` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `ker` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `quotientKerEquivOfRightInverse` `instNonAssocSemiringQuotient` `kerLift`	—	—
`quotientKerEquivOfSurjective_mk` 📖	mathematical	`DFunLike.coe` `RingHom` `RingHom.instFunLike`	`RingEquiv` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `ker` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `quotientKerEquivOfSurjective` `toQuotient`	—	—
`quotientKerEquivRangeₐ_comp_mkₐ` 📖	mathematical	—	`AlgHom.comp` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `ker` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `instSemiringQuotient` `Subalgebra.toSemiring` `instAlgebraQuotient` `Subalgebra.algebra` `AlgEquiv.toAlgHom` `quotientKerEquivRangeₐ` `mkₐ` `AlgHom.rangeRestrict`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`quotientKerEquivRangeₐ_mkₐ` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `ker` `RingHomClass.toRingHom` `AlgHom` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Subalgebra` `SetLike.instMembership` `Subalgebra.instSetLike` `AlgHom.range` `instSemiringQuotient` `Subalgebra.toSemiring` `instAlgebraQuotient` `Subalgebra.algebra` `AlgEquiv.instFunLike` `quotientKerEquivRangeₐ` `toQuotient` `AlgHom.mem_range_self`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`quotientQuotientEquivQuotient_coe_coe` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `RingEquiv` `Quotient` `instNonAssocSemiringQuotient` `ker` `map` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `quotientQuotientEquivQuotient` `toQuotient`	—	—
`quotientQuotientEquivQuotient_mk_mk` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `RingEquiv` `Quotient` `instNonAssocSemiringQuotient` `ker` `map` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `quotientQuotientEquivQuotient` `Con.toSetoid` `toCon`	—	—
`quotientQuotientEquivQuotient_symm_mk` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `RingEquiv` `Quotient` `instNonAssocSemiringQuotient` `ker` `map` `instMulQuotient` `instAddQuotient` `EquivLike.toFunLike` `RingEquiv.instEquivLike` `RingEquiv.symm` `quotientQuotientEquivQuotient` `Con.toSetoid` `toCon`	—	—
`quotientQuotientEquivQuotientₐ_coe_coe` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `AlgEquiv` `Quotient` `instNonAssocSemiringQuotient` `ker` `RingHomClass.toRingHom` `AlgHom` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `factorₐ` `AlgEquiv.instFunLike` `quotientQuotientEquivQuotientₐ` `toQuotient`	—	—
`quotientQuotientEquivQuotientₐ_mk_mk` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `AlgEquiv` `Quotient` `instNonAssocSemiringQuotient` `ker` `RingHomClass.toRingHom` `AlgHom` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `factorₐ` `AlgEquiv.instFunLike` `quotientQuotientEquivQuotientₐ` `Con.toSetoid` `toCon`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`quotientQuotientEquivQuotientₐ_symm_mk` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instLE`	`DFunLike.coe` `AlgEquiv` `Quotient` `instNonAssocSemiringQuotient` `ker` `RingHomClass.toRingHom` `AlgHom` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `factorₐ` `AlgEquiv.instFunLike` `AlgEquiv.symm` `quotientQuotientEquivQuotientₐ` `Con.toSetoid` `toCon`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass`
`rangeS_kerLift` 📖	mathematical	—	`RingHom.rangeS` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `ker` `instNonAssocSemiringQuotient` `kerLift`	—	`rangeS_lift`
`rangeS_lift` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instLE` `ker`	`RingHom.rangeS` `Quotient` `instNonAssocSemiringQuotient` `lift`	—	`SetLike.coe_injective` `Set.range_quot_lift`
`rangeS_mk'` 📖	mathematical	—	`RingHom.rangeS` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `instNonAssocSemiringQuotient` `mk'` `Top.top` `Subsemiring` `Subsemiring.instTop`	—	`RingHom.rangeS_eq_top` `mk'_surjective`
`range_lift` 📖	mathematical	`RingCon` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Distrib.toMul` `instLE` `ker` `Semiring.toNonAssocSemiring` `Ring.toSemiring`	`RingHom.range` `Quotient` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `instRingQuotient` `lift`	—	`SetLike.coe_injective` `Set.range_quot_lift`
`range_mk'` 📖	mathematical	—	`RingHom.range` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Ring.toSemiring` `Distrib.toMul` `instRingQuotient` `mk'` `Top.top` `Subring` `Subring.instTop`	—	`RingHom.range_eq_top` `mk'_surjective`
`range_mkₐ` 📖	mathematical	—	`AlgHom.range` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instSemiringQuotient` `instAlgebraQuotient` `mkₐ` `Top.top` `Subalgebra` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Algebra.instCompleteLatticeSubalgebra` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	`AlgHom.range_eq_top` `mkₐ_surjective`

RingCon.Quotient

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`hom_ext` 📖	—	`RingHom.comp` `RingCon.Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `RingCon.instNonAssocSemiringQuotient` `RingCon.mk'`	—	—	`DFunLike.ext` `Function.Surjective.forall` `RingCon.mk'_surjective`
`hom_ext_iff` 📖	mathematical	—	`RingHom.comp` `RingCon.Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Distrib.toMul` `RingCon.instNonAssocSemiringQuotient` `RingCon.mk'`	—	`hom_ext`

---

← Back to Index