RingQuot

📁 Source: Mathlib/Algebra/RingQuot.lean

Statistics

Metric	Count
Definitions `instAlgebraQuotient`, `mkₐ`, `idealQuotientToRingQuot`, `instAdd`, `instAddCommMonoid`, `instAlgebra`, `instCommRing`, `instCommSemiring`, `instInhabited`, `instMonoidWithZero`, `instMul`, `instNatCast`, `instNatPow`, `instNeg`, `instOne`, `instRing`, `instSMulOfAlgebra`, `instSemiring`, `instSub`, `instZero`, `intCast`, `liftAlgHom`, `mkAlgHom`, `mkRingHom`, `natCast`, `preLift`, `preLiftAlgHom`, `ringCon`, `ringQuotEquivIdealQuotient`, `ringQuotToIdealQuotient`, `smul`, `toQuot`	32
Theorems `coe_algebraMap`, `mkₐ_apply`, `mkₐ_surjective`, `add_right`, `neg`, `smul`, `sub_left`, `sub_right`, `add_quot`, `eq_liftAlgHom_comp_mkAlgHom`, `eq_lift_comp_mkRingHom`, `eqvGen_rel_eq`, `idealQuotientToRingQuot_apply`, `instIsScalarTower`, `instSMulCommClass`, `liftAlgHom_def`, `liftAlgHom_mkAlgHom_apply`, `liftAlgHom_unique`, `lift_def`, `lift_mkRingHom_apply`, `lift_unique`, `mkAlgHom_coe`, `mkAlgHom_def`, `mkAlgHom_rel`, `mkAlgHom_surjective`, `mkRingHom_def`, `mkRingHom_rel`, `mkRingHom_surjective`, `mul_quot`, `neg_quot`, `one_quot`, `pow_quot`, `preLiftAlgHom_def`, `preLift_def`, `ringQuotToIdealQuotient_apply`, `ringQuot_ext`, `ringQuot_ext'`, `ringQuot_ext'_iff`, `ringQuot_ext_iff`, `smul_quot`, `sub_quot`, `zero_quot`	42
Total	74

RingCon

Definitions

Name	Category	Theorems
`instAlgebraQuotient` 📖	CompOp	24 math math: `quotientKerEquivRangeₐ_comp_mkₐ`, `coe_comapQuotientEquivRangeₐ_mk`, `mkₐ_comp_factorₐ_comp_mkₐ`, `kerLiftₐ_mk`, `factorₐ_mk`, `coe_algebraMap`, `congrₐ_mk`, `kerLiftₐ_injective`, `kerLiftₐ_range_eq`, `quotientQuotientEquivQuotientₐ_mk_mk`, `coe_comapQuotientEquivRangeₐ_symm_mk`, `mkₐ_apply`, `comapQuotientEquivRangeₐ_mk`, `factorₐ_apply`, `mkₐ_surjective`, `quotientQuotientEquivQuotientₐ_symm_mk`, `quotientKerEquivRangeₐ_mkₐ`, `liftₐ_range`, `range_mkₐ`, `liftₐ_mk`, `coe_liftₐ`, `quotientQuotientEquivQuotientₐ_coe_coe`, `liftₐ_coe_toRingHom`, `coe_quotientKerEquivRangeₐ_mkₐ`
`mkₐ` 📖	CompOp	9 math math: `quotientKerEquivRangeₐ_comp_mkₐ`, `coe_comapQuotientEquivRangeₐ_mk`, `mkₐ_comp_factorₐ_comp_mkₐ`, `coe_comapQuotientEquivRangeₐ_symm_mk`, `mkₐ_apply`, `comapQuotientEquivRangeₐ_mk`, `factorₐ_apply`, `mkₐ_surjective`, `range_mkₐ`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_algebraMap` 📖	mathematical	—	`toQuotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `DFunLike.coe` `RingHom` `CommSemiring.toSemiring` `RingHom.instFunLike` `algebraMap` `Quotient` `instSemiringQuotient` `instAlgebraQuotient`	—	—
`mkₐ_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `mkₐ` `toQuotient`	—	—
`mkₐ_surjective` 📖	mathematical	—	`Quotient` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul` `DFunLike.coe` `AlgHom` `instSemiringQuotient` `instAlgebraQuotient` `AlgHom.funLike` `mkₐ`	—	`mk'_surjective`

RingQuot

Definitions

Name	Category	Theorems
`idealQuotientToRingQuot` 📖	CompOp	1 math math: `idealQuotientToRingQuot_apply`
`instAdd` 📖	CompOp	1 math math: `add_quot`
`instAddCommMonoid` 📖	CompOp	19 math math: `SymmetricAlgebra.lift_ι_apply`, `SymmetricAlgebra.rank_eq`, `LinearAlgebra.FreeProduct.mul_injections`, `SymmetricAlgebra.instModuleFree`, `LinearAlgebra.FreeProduct.ι_apply`, `IsSymmetricAlgebra.equiv_symm_comp`, `LinearAlgebra.FreeProduct.identify_one`, `IsSymmetricAlgebra.equiv_symm_apply`, `SymmetricAlgebra.algHom_ext_iff`, `SymmetricAlgebra.equivMvPolynomial_symm_X`, `SymmetricAlgebra.lift_comp_ι`, `DividedPowerAlgebra.submodule_span_prod_dp_eq_top`, `Module.Basis.symmetricAlgebra_repr_apply`, `SymmetricAlgebra.equivMvPolynomial_ι_apply`, `DividedPowerAlgebra.dp_sum_smul`, `DividedPowerAlgebra.dp_sum`, `LinearAlgebra.FreeProduct.lof_map_one`, `DividedPowerAlgebra.dp_add`, `DividedPowerAlgebra.embed_def`
`instAlgebra` 📖	CompOp	39 math math: `SymmetricAlgebra.lift_ι_apply`, `SymmetricAlgebra.rank_eq`, `SymmetricAlgebra.isSymmetricAlgebra_ι`, `IsSymmetricAlgebra.equiv_apply`, `TensorAlgebra.ι_def`, `mkAlgHom_surjective`, `ringQuot_ext'_iff`, `SymmetricAlgebra.instModuleFree`, `IsSymmetricAlgebra.equiv_symm_comp`, `liftAlgHom_def`, `liftAlgHom_mkAlgHom_apply`, `SymmetricAlgebra.algebraMap_eq_zero_iff`, `liftAlgHom_unique`, `IsSymmetricAlgebra.equiv_symm_apply`, `SymmetricAlgebra.algHom_ext_iff`, `SymmetricAlgebra.equivMvPolynomial_symm_X`, `SymmetricAlgebra.lift_comp_ι`, `DividedPowerAlgebra.mkAlgHom_surjective`, `SymmetricAlgebra.lift_ι`, `DividedPowerAlgebra.submodule_span_prod_dp_eq_top`, `Module.Basis.symmetricAlgebra_repr_apply`, `DividedPowerAlgebra.algHom_ext_iff`, `SymmetricAlgebra.equivMvPolynomial_ι_apply`, `SymmetricAlgebra.algebraMap_eq_one_iff`, `mkAlgHom_rel`, `DividedPowerAlgebra.dp_def`, `SymmetricAlgebra.algHom_surjective`, `SymmetricAlgebra.algebraMap_leftInverse`, `preLiftAlgHom_def`, `SymmetricAlgebra.algebraMap_inj`, `LinearAlgebra.FreeProduct.lift_apply`, `IsSymmetricAlgebra.comp_equiv`, `IsSymmetricAlgebra.equiv_toAlgHom`, `TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι`, `DividedPowerAlgebra.mkRingHom_C`, `DividedPowerAlgebra.mkAlgHom_C`, `DividedPowerAlgebra.embed_def`, `eq_liftAlgHom_comp_mkAlgHom`, `mkAlgHom_coe`
`instCommRing` 📖	CompOp	1 math math: `DividedPowerAlgebra.submodule_span_prod_dp_eq_top`
`instCommSemiring` 📖	CompOp	3 math math: `DividedPowerAlgebra.dp_sum_smul`, `DividedPowerAlgebra.dp_sum`, `DividedPowerAlgebra.prod_dp`
`instInhabited` 📖	CompOp	—
`instMonoidWithZero` 📖	CompOp	1 math math: `DividedPowerAlgebra.natFactorial_mul_dp_eq`
`instMul` 📖	CompOp	7 math math: `LinearAlgebra.FreeProduct.mul_injections`, `DividedPowerAlgebra.dp_mul`, `mul_quot`, `DividedPowerAlgebra.natFactorial_mul_dp_eq`, `SymmetricAlgebra.instNoZeroDivisors`, `DividedPowerAlgebra.dp_add`, `DividedPowerAlgebra.prod_dp`
`instNatCast` 📖	CompOp	2 math math: `DividedPowerAlgebra.natFactorial_mul_dp_eq`, `DividedPowerAlgebra.prod_dp`
`instNatPow` 📖	CompOp	1 math math: `pow_quot`
`instNeg` 📖	CompOp	1 math math: `neg_quot`
`instOne` 📖	CompOp	6 math math: `LinearAlgebra.FreeProduct.identify_one`, `DividedPowerAlgebra.dp_zero`, `SymmetricAlgebra.algebraMap_eq_one_iff`, `LinearAlgebra.FreeProduct.lof_map_one`, `one_quot`, `DividedPowerAlgebra.dp_null`
`instRing` 📖	CompOp	—
`instSMulOfAlgebra` 📖	CompOp	5 math math: `instIsScalarTower`, `instSMulCommClass`, `DividedPowerAlgebra.dp_sum_smul`, `smul_quot`, `DividedPowerAlgebra.dp_smul`
`instSemiring` 📖	CompOp	52 math math: `SymmetricAlgebra.lift_ι_apply`, `SymmetricAlgebra.rank_eq`, `IsSymmetricAlgebra.equiv_apply`, `TensorAlgebra.ι_def`, `mkAlgHom_surjective`, `ringQuot_ext'_iff`, `SymmetricAlgebra.instModuleFree`, `DividedPowerAlgebra.dp_mul`, `preLift_def`, `mkRingHom_def`, `idealQuotientToRingQuot_apply`, `IsSymmetricAlgebra.equiv_symm_comp`, `liftAlgHom_def`, `eq_lift_comp_mkRingHom`, `liftAlgHom_mkAlgHom_apply`, `lift_unique`, `SymmetricAlgebra.algebraMap_eq_zero_iff`, `liftAlgHom_unique`, `lift_mkRingHom_apply`, `lift_def`, `IsSymmetricAlgebra.equiv_symm_apply`, `ringQuot_ext_iff`, `SymmetricAlgebra.algHom_ext_iff`, `SymmetricAlgebra.equivMvPolynomial_symm_X`, `SymmetricAlgebra.lift_comp_ι`, `DividedPowerAlgebra.mkAlgHom_surjective`, `SymmetricAlgebra.lift_ι`, `DividedPowerAlgebra.submodule_span_prod_dp_eq_top`, `Module.Basis.symmetricAlgebra_repr_apply`, `SymmetricAlgebra.instIsDomain`, `DividedPowerAlgebra.algHom_ext_iff`, `SymmetricAlgebra.equivMvPolynomial_ι_apply`, `mkRingHom_surjective`, `SymmetricAlgebra.algebraMap_eq_one_iff`, `mkAlgHom_rel`, `DividedPowerAlgebra.dp_def`, `SymmetricAlgebra.algHom_surjective`, `SymmetricAlgebra.algebraMap_leftInverse`, `preLiftAlgHom_def`, `SymmetricAlgebra.algebraMap_inj`, `LinearAlgebra.FreeProduct.lift_apply`, `IsSymmetricAlgebra.comp_equiv`, `IsSymmetricAlgebra.equiv_toAlgHom`, `TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι`, `DividedPowerAlgebra.mkRingHom_C`, `DividedPowerAlgebra.mkAlgHom_C`, `DividedPowerAlgebra.embed_def`, `mkRingHom_rel`, `eq_liftAlgHom_comp_mkAlgHom`, `mkAlgHom_coe`, `DividedPowerAlgebra.dp_eq_mkRingHom`, `ringQuotToIdealQuotient_apply`
`instSub` 📖	CompOp	1 math math: `sub_quot`
`instZero` 📖	CompOp	5 math math: `SymmetricAlgebra.algebraMap_eq_zero_iff`, `zero_quot`, `SymmetricAlgebra.instNoZeroDivisors`, `DividedPowerAlgebra.dp_null_of_ne_zero`, `DividedPowerAlgebra.dp_null`
`intCast` 📖	CompOp	—
`liftAlgHom` 📖	CompOp	5 math math: `liftAlgHom_def`, `liftAlgHom_mkAlgHom_apply`, `liftAlgHom_unique`, `LinearAlgebra.FreeProduct.lift_apply`, `eq_liftAlgHom_comp_mkAlgHom`
`mkAlgHom` 📖	CompOp	13 math math: `TensorAlgebra.ι_def`, `mkAlgHom_surjective`, `ringQuot_ext'_iff`, `mkAlgHom_def`, `liftAlgHom_def`, `liftAlgHom_mkAlgHom_apply`, `DividedPowerAlgebra.mkAlgHom_surjective`, `mkAlgHom_rel`, `DividedPowerAlgebra.dp_def`, `TensorAlgebra.ringQuot_mkAlgHom_freeAlgebra_ι_eq_ι`, `DividedPowerAlgebra.mkAlgHom_C`, `eq_liftAlgHom_comp_mkAlgHom`, `mkAlgHom_coe`
`mkRingHom` 📖	CompOp	12 math math: `mkRingHom_def`, `idealQuotientToRingQuot_apply`, `eq_lift_comp_mkRingHom`, `lift_mkRingHom_apply`, `lift_def`, `ringQuot_ext_iff`, `mkRingHom_surjective`, `DividedPowerAlgebra.mkRingHom_C`, `mkRingHom_rel`, `mkAlgHom_coe`, `DividedPowerAlgebra.dp_eq_mkRingHom`, `ringQuotToIdealQuotient_apply`
`natCast` 📖	CompOp	—
`preLift` 📖	CompOp	2 math math: `preLift_def`, `lift_def`
`preLiftAlgHom` 📖	CompOp	2 math math: `liftAlgHom_def`, `preLiftAlgHom_def`
`ringCon` 📖	CompOp	—
`ringQuotEquivIdealQuotient` 📖	CompOp	—
`ringQuotToIdealQuotient` 📖	CompOp	1 math math: `ringQuotToIdealQuotient_apply`
`smul` 📖	CompOp	—
`toQuot` 📖	CompOp	3 math math: `preLift_def`, `preLiftAlgHom_def`, `ExteriorAlgebra.invertibleAlgebraMapEquiv_symm_apply_invOf_toQuot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_quot` 📖	mathematical	—	`RingQuot` `instAdd` `Rel` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`eq_liftAlgHom_comp_mkAlgHom` 📖	mathematical	—	`DFunLike.coe` `Equiv` `AlgHom` `RingQuot` `instSemiring` `instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftAlgHom` `AlgHom.comp` `mkAlgHom` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHomClass.toRingHom` `AlgHom.funLike` `mkAlgHom_rel`	—	`liftAlgHom_unique` `mkAlgHom_rel`
`eq_lift_comp_mkRingHom` 📖	mathematical	—	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `RingQuot` `instSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `RingHom.comp` `mkRingHom` `RingHom.instFunLike` `mkRingHom_rel`	—	`lift_unique` `mkRingHom_rel`
`eqvGen_rel_eq` 📖	mathematical	—	`Relation.EqvGen` `Rel` `RingConGen.Rel` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `Distrib.toMul`	—	`RingCon.refl` `RingCon.symm` `RingCon.trans` `RingCon.add` `RingCon.mul`
`idealQuotientToRingQuot_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `HasQuotient.Quotient` `Ideal` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Ideal.instHasQuotient_1` `Ideal.ofRel` `RingQuot` `Semiring.toNonAssocSemiring` `Ideal.Quotient.semiring` `instSemiring` `RingHom.instFunLike` `idealQuotientToRingQuot` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1` `mkRingHom`	—	`Ideal.instIsTwoSided_1`
`instIsScalarTower` 📖	mathematical	—	`IsScalarTower` `RingQuot` `instSMulOfAlgebra`	—	`smul_quot` `smul_assoc`
`instSMulCommClass` 📖	mathematical	—	`SMulCommClass` `RingQuot` `instSMulOfAlgebra`	—	`smul_quot` `SMulCommClass.smul_comm`
`liftAlgHom_def` 📖	mathematical	—	`liftAlgHom` `AlgHom` `RingQuot` `instSemiring` `instAlgebra` `preLiftAlgHom` `AlgHom.comp` `mkAlgHom`	—	—
`liftAlgHom_mkAlgHom_apply` 📖	mathematical	`DFunLike.coe` `AlgHom` `AlgHom.funLike`	`DFunLike.coe` `AlgHom` `RingQuot` `instSemiring` `instAlgebra` `AlgHom.funLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftAlgHom` `mkAlgHom`	—	`liftAlgHom_def` `preLiftAlgHom_def` `mkAlgHom_def` `mkRingHom_def`
`liftAlgHom_unique` 📖	mathematical	`DFunLike.coe` `AlgHom` `AlgHom.funLike` `AlgHom.comp` `RingQuot` `instSemiring` `instAlgebra` `mkAlgHom`	`DFunLike.coe` `Equiv` `AlgHom` `RingQuot` `instSemiring` `instAlgebra` `EquivLike.toFunLike` `Equiv.instEquivLike` `liftAlgHom`	—	`ringQuot_ext'` `AlgHom.ext` `liftAlgHom_mkAlgHom_apply`
`lift_def` 📖	mathematical	—	`lift` `RingHom` `Semiring.toNonAssocSemiring` `RingQuot` `instSemiring` `preLift` `RingHom.comp` `mkRingHom`	—	—
`lift_mkRingHom_apply` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`DFunLike.coe` `RingHom` `RingQuot` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `Equiv` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift` `mkRingHom`	—	`lift_def` `preLift_def` `mkRingHom_def`
`lift_unique` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHom.comp` `RingQuot` `instSemiring` `mkRingHom`	`DFunLike.coe` `Equiv` `RingHom` `Semiring.toNonAssocSemiring` `RingQuot` `instSemiring` `EquivLike.toFunLike` `Equiv.instEquivLike` `lift`	—	`ringQuot_ext` `RingHom.ext` `lift_mkRingHom_apply`
`mkAlgHom_coe` 📖	mathematical	—	`RingHomClass.toRingHom` `AlgHom` `RingQuot` `instSemiring` `instAlgebra` `AlgHom.funLike` `Semiring.toNonAssocSemiring` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `mkAlgHom` `mkRingHom`	—	`AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `RingHomClass.toRingHom.congr_simp` `mkAlgHom_def` `mkRingHom_def`
`mkAlgHom_def` 📖	mathematical	—	`mkAlgHom`	—	—
`mkAlgHom_rel` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `RingQuot` `instSemiring` `instAlgebra` `AlgHom.funLike` `mkAlgHom`	—	`mkRingHom_def` `mkAlgHom_def`
`mkAlgHom_surjective` 📖	mathematical	—	`RingQuot` `DFunLike.coe` `AlgHom` `instSemiring` `instAlgebra` `AlgHom.funLike` `mkAlgHom`	—	`mkRingHom_def` `mkAlgHom_def`
`mkRingHom_def` 📖	mathematical	—	`mkRingHom` `RingQuot` `Semiring.toNonAssocSemiring` `instSemiring` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toOne` `Rel`	—	—
`mkRingHom_rel` 📖	mathematical	—	`DFunLike.coe` `RingHom` `RingQuot` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `mkRingHom`	—	`mkRingHom_def`
`mkRingHom_surjective` 📖	mathematical	—	`RingQuot` `DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `instSemiring` `RingHom.instFunLike` `mkRingHom`	—	`mkRingHom_def`
`mul_quot` 📖	mathematical	—	`RingQuot` `instMul` `Rel` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	—
`neg_quot` 📖	mathematical	—	`RingQuot` `Ring.toSemiring` `instNeg` `Rel` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	—
`one_quot` 📖	mathematical	—	`Rel` `AddMonoidWithOne.toOne` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `RingQuot` `instOne`	—	—
`pow_quot` 📖	mathematical	—	`RingQuot` `instNatPow` `Rel` `Monoid.toPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	—
`preLiftAlgHom_def` 📖	mathematical	`DFunLike.coe` `AlgHom` `AlgHom.funLike`	`preLiftAlgHom` `RingQuot` `instSemiring` `instAlgebra` `Semiring.toNonAssocSemiring` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toOne` `Rel` `DFunLike.coe` `AlgHom` `AlgHom.funLike` `toQuot`	—	—
`preLift_def` 📖	mathematical	`DFunLike.coe` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike`	`preLift` `RingQuot` `Semiring.toNonAssocSemiring` `instSemiring` `MulOneClass.toMulOne` `MulZeroOneClass.toMulOneClass` `NonAssocSemiring.toMulZeroOneClass` `MulOne.toOne` `Rel` `DFunLike.coe` `RingHom` `RingHom.instFunLike` `toQuot`	—	—
`ringQuotToIdealQuotient_apply` 📖	mathematical	—	`DFunLike.coe` `RingHom` `RingQuot` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `HasQuotient.Quotient` `Ideal` `Ideal.instHasQuotient_1` `Ideal.ofRel` `Semiring.toNonAssocSemiring` `instSemiring` `Ideal.Quotient.semiring` `RingHom.instFunLike` `ringQuotToIdealQuotient` `mkRingHom` `Ring.toSemiring` `CommRing.toRing` `Ideal.instHasQuotient` `Ideal.Quotient.ring` `Ideal.instIsTwoSided_1`	—	`Ideal.instIsTwoSided_1` `lift_def` `preLift_def` `mkRingHom_def`
`ringQuot_ext` 📖	—	`RingHom.comp` `RingQuot` `Semiring.toNonAssocSemiring` `instSemiring` `mkRingHom`	—	—	`RingHom.ext` `mkRingHom_surjective` `RingHom.congr_fun`
`ringQuot_ext'` 📖	—	`AlgHom.comp` `RingQuot` `instSemiring` `instAlgebra` `mkAlgHom`	—	—	`AlgHom.ext` `mkAlgHom_surjective` `AlgHom.congr_fun`
`ringQuot_ext'_iff` 📖	mathematical	—	`AlgHom.comp` `RingQuot` `instSemiring` `instAlgebra` `mkAlgHom`	—	`ringQuot_ext'`
`ringQuot_ext_iff` 📖	mathematical	—	`RingHom.comp` `RingQuot` `Semiring.toNonAssocSemiring` `instSemiring` `mkRingHom`	—	`ringQuot_ext`
`smul_quot` 📖	mathematical	—	`RingQuot` `instSMulOfAlgebra` `Rel` `Algebra.toSMul`	—	—
`sub_quot` 📖	mathematical	—	`RingQuot` `Ring.toSemiring` `instSub` `Rel` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	—
`zero_quot` 📖	mathematical	—	`Rel` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring` `RingQuot` `instZero`	—	—

RingQuot.Rel

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`add_right` 📖	mathematical	`RingQuot.Rel`	`RingQuot.Rel` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `Semiring.toNonAssocSemiring`	—	`add_comm`
`neg` 📖	mathematical	`RingQuot.Rel` `Ring.toSemiring`	`RingQuot.Rel` `Ring.toSemiring` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`neg_eq_neg_one_mul`
`smul` 📖	mathematical	`RingQuot.Rel`	`RingQuot.Rel` `Algebra.toSMul`	—	`Algebra.smul_def`
`sub_left` 📖	mathematical	`RingQuot.Rel` `Ring.toSemiring`	`RingQuot.Rel` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sub_eq_add_neg`
`sub_right` 📖	mathematical	`RingQuot.Rel` `Ring.toSemiring`	`RingQuot.Rel` `Ring.toSemiring` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`sub_eq_add_neg` `add_right` `neg`

---

← Back to Index