Basic

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

Statistics

Metric	Count
Definitions `gi`, `instCompleteLattice`, `instDistribMulActionQuotientOfIsScalarTower`, `instInfSet`, `instLE`, `instMulSemiringActionQuotientOfIsScalarTower`, `instPartialOrder`, `instSMulQuotient`	8
Theorems `coe_bot`, `coe_iInf`, `coe_inf`, `coe_sInf`, `coe_smul`, `coe_top`, `comap_mono`, `inf_iff_and`, `instIsCentralScalarQuotient`, `instIsScalarTowerQuotient`, `instNontrivial`, `instSMulCommClassQuotient`, `instSubsingleton`, `isScalarTower_right`, `le_def`, `nontrivial_iff`, `nontrivial_quotient`, `ringConGen_eq`, `ringConGen_idem`, `ringConGen_le`, `ringConGen_mono`, `ringConGen_of_ringCon`, `sInf_toSetoid`, `sSup_def`, `sSup_eq_ringConGen`, `smulCommClass`, `smulCommClass'`, `subsingleton_iff`, `subsingleton_quotient`, `sup_def`, `sup_eq_ringConGen`, `toCon_bot`, `toCon_eq_bot`, `toCon_eq_top`, `toCon_top`	35
Total	43

RingCon

Definitions

Name	Category	Theorems
`gi` 📖	CompOp	—
`instCompleteLattice` 📖	CompOp	22 math math: `toCon_eq_bot`, `sSup_def`, `comap_bot`, `matrix_top`, `TwoSidedIdeal.iSup_ringCon`, `sup_def`, `subsingleton_quotient`, `inf_iff_and`, `coe_inf`, `sSup_eq_ringConGen`, `TwoSidedIdeal.sSup_ringCon`, `matrix_bot`, `coe_bot`, `TwoSidedIdeal.top_ringCon`, `TwoSidedIdeal.sup_ringCon`, `toCon_eq_top`, `TwoSidedIdeal.bot_ringCon`, `coe_top`, `TwoSidedIdeal.inf_ringCon`, `sup_eq_ringConGen`, `toCon_bot`, `toCon_top`
`instDistribMulActionQuotientOfIsScalarTower` 📖	CompOp	—
`instInfSet` 📖	CompOp	6 math math: `TwoSidedIdeal.iInf_ringCon`, `ringConGen_eq`, `sInf_toSetoid`, `TwoSidedIdeal.sInf_ringCon`, `coe_iInf`, `coe_sInf`
`instLE` 📖	CompOp	8 math math: `TwoSidedIdeal.orderIsoRingCon_symm_apply`, `TwoSidedIdeal.ringCon_le_iff`, `TwoSidedIdeal.orderIsoRingCon_apply`, `opOrderIso_apply`, `le_def`, `opOrderIso_symm_apply`, `ringConGen_le`, `ringConGen_mono`
`instMulSemiringActionQuotientOfIsScalarTower` 📖	CompOp	—
`instPartialOrder` 📖	CompOp	2 math math: `matrix_strictMono_of_nonempty`, `matrix_monotone`
`instSMulQuotient` 📖	CompOp	7 math math: `smulCommClass`, `instSMulCommClassQuotient`, `isScalarTower_right`, `instIsScalarTowerQuotient`, `coe_smul`, `smulCommClass'`, `instIsCentralScalarQuotient`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_bot` 📖	mathematical	—	`DFunLike.coe` `RingCon` `instFunLikeForallProp` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	—
`coe_iInf` 📖	mathematical	—	`DFunLike.coe` `RingCon` `instFunLikeForallProp` `iInf` `instInfSet` `Pi.infSet` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Prop.instCompleteLattice`	—	`iInf.eq_1` `coe_sInf` `Set.range_comp` `sInf_range`
`coe_inf` 📖	mathematical	—	`DFunLike.coe` `RingCon` `instFunLikeForallProp` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `instCompleteLattice` `Pi.instMinForall_mathlib` `Prop.instCompleteLattice`	—	—
`coe_sInf` 📖	mathematical	—	`DFunLike.coe` `RingCon` `instFunLikeForallProp` `InfSet.sInf` `instInfSet` `Pi.infSet` `CompleteSemilatticeInf.toInfSet` `CompleteLattice.toCompleteSemilatticeInf` `Prop.instCompleteLattice` `Set.image`	—	`sInf_image` `iInf_apply` `iInf_Prop_eq`
`coe_smul` 📖	mathematical	—	`toQuotient` `MulOne.toMul` `MulOneClass.toMulOne` `Quotient` `instSMulQuotient`	—	—
`coe_top` 📖	mathematical	—	`DFunLike.coe` `RingCon` `instFunLikeForallProp` `Top.top` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Pi.instTopForall` `BooleanAlgebra.toTop` `Prop.instBooleanAlgebra`	—	—
`comap_mono` 📖	mathematical	`RingCon` `instLE`	`comap`	—	—
`inf_iff_and` 📖	mathematical	—	`DFunLike.coe` `RingCon` `instFunLikeForallProp` `SemilatticeInf.toMin` `Lattice.toSemilatticeInf` `CompleteLattice.toLattice` `instCompleteLattice`	—	—
`instIsCentralScalarQuotient` 📖	mathematical	—	`IsCentralScalar` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instSMulQuotient` `MulOpposite` `IsScalarTower.op_left`	—	`IsScalarTower.op_left` `Con.instIsCentralScalar`
`instIsScalarTowerQuotient` 📖	mathematical	—	`IsScalarTower` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instSMulQuotient`	—	`Con.instIsScalarTower`
`instNontrivial` 📖	mathematical	—	`Nontrivial` `RingCon`	—	`exists_pair_ne`
`instSMulCommClassQuotient` 📖	mathematical	—	`SMulCommClass` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instSMulQuotient`	—	`Con.instSMulCommClass`
`instSubsingleton` 📖	mathematical	—	`RingCon`	—	`ext` `refl`
`isScalarTower_right` 📖	mathematical	—	`IsScalarTower` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instSMulQuotient` `instMulQuotient`	—	`Quotient.ind₂'` `smul_mul_assoc`
`le_def` 📖	mathematical	—	`RingCon` `instLE` `DFunLike.coe` `instFunLikeForallProp`	—	—
`nontrivial_iff` 📖	mathematical	—	`Nontrivial` `RingCon`	—	`subsingleton_or_nontrivial` `instSubsingleton` `instNontrivial`
`nontrivial_quotient` 📖	mathematical	—	`Nontrivial` `Quotient`	—	—
`ringConGen_eq` 📖	mathematical	—	`ringConGen` `InfSet.sInf` `RingCon` `instInfSet` `setOf`	—	`le_antisymm` `refl` `symm` `trans` `add` `mul` `sInf_le`
`ringConGen_idem` 📖	mathematical	—	`ringConGen` `DFunLike.coe` `RingCon` `instFunLikeForallProp`	—	`ringConGen_of_ringCon`
`ringConGen_le` 📖	mathematical	`DFunLike.coe` `RingCon` `instFunLikeForallProp`	`instLE` `ringConGen`	—	`ringConGen_eq` `sInf_le`
`ringConGen_mono` 📖	mathematical	—	`RingCon` `instLE` `ringConGen`	—	`ringConGen_le`
`ringConGen_of_ringCon` 📖	mathematical	—	`ringConGen` `DFunLike.coe` `RingCon` `instFunLikeForallProp`	—	`le_antisymm` `ringConGen_eq` `sInf_le`
`sInf_toSetoid` 📖	mathematical	—	`Con.toSetoid` `toCon` `InfSet.sInf` `RingCon` `instInfSet` `Setoid.instInfSet` `Set.image`	—	`Setoid.ext`
`sSup_def` 📖	mathematical	—	`SupSet.sSup` `RingCon` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `ringConGen` `Pi.supSet` `Prop.instCompleteLattice` `Set.image` `DFunLike.coe` `instFunLikeForallProp`	—	`sSup_eq_ringConGen` `sSup_image` `iSup_apply` `iSup_Prop_eq`
`sSup_eq_ringConGen` 📖	mathematical	—	`SupSet.sSup` `RingCon` `CompleteSemilatticeSup.toSupSet` `CompleteLattice.toCompleteSemilatticeSup` `instCompleteLattice` `ringConGen` `Set` `Set.instMembership` `DFunLike.coe` `instFunLikeForallProp`	—	`ringConGen_eq` `Set.ext`
`smulCommClass` 📖	mathematical	—	`SMulCommClass` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instSMulQuotient` `instMulQuotient`	—	`Quotient.ind₂'` `mul_smul_comm`
`smulCommClass'` 📖	mathematical	—	`SMulCommClass` `Quotient` `MulOne.toMul` `MulOneClass.toMulOne` `instMulQuotient` `instSMulQuotient`	—	`SMulCommClass.symm` `smulCommClass`
`subsingleton_iff` 📖	mathematical	—	`RingCon`	—	—
`subsingleton_quotient` 📖	mathematical	—	`Quotient` `Top.top` `RingCon` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder`	—	—
`sup_def` 📖	mathematical	—	`RingCon` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `ringConGen` `Pi.instMaxForall_mathlib` `Prop.instCompleteLattice` `DFunLike.coe` `instFunLikeForallProp`	—	`sup_eq_ringConGen`
`sup_eq_ringConGen` 📖	mathematical	—	`RingCon` `SemilatticeSup.toMax` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `ringConGen` `DFunLike.coe` `instFunLikeForallProp`	—	`ringConGen_eq`
`toCon_bot` 📖	mathematical	—	`toCon` `Bot.bot` `RingCon` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Con` `Con.instCompleteLattice`	—	—
`toCon_eq_bot` 📖	mathematical	—	`toCon` `Bot.bot` `Con` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Con.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `RingCon` `instCompleteLattice`	—	`toCon_bot`
`toCon_eq_top` 📖	mathematical	—	`toCon` `Top.top` `Con` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Con.instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `RingCon` `instCompleteLattice`	—	`toCon_top`
`toCon_top` 📖	mathematical	—	`toCon` `Top.top` `RingCon` `OrderTop.toTop` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderTop` `CompleteLattice.toBoundedOrder` `Con` `Con.instCompleteLattice`	—	—

---

← Back to Index