StandardPart

📁 Source: Mathlib/Algebra/Order/Ring/StandardPart.lean

Statistics

Metric	Count
Definitions `FiniteElement`, `instCommRing`, `instFloorRing`, `instLinearOrder`, `instRatCast`, `mk`, `FiniteResidueField`, `instField`, `instLinearOrder`, `mk`, `ofArchimedean`, `stdPart`	12
Theorems `ext`, `ext_iff`, `instIsDomain`, `instIsStrictOrderedRing`, `instValuationRing`, `isUnit_iff_mk_eq_zero`, `mk_add_mk`, `mk_intCast`, `mk_le_mk`, `mk_lt_mk`, `mk_mul_mk`, `mk_natCast`, `mk_neg`, `mk_one`, `mk_ratCast`, `mk_sub_mk`, `mk_zero`, `neg_mk`, `not_isUnit_iff_mk_pos`, `val_add`, `val_mul`, `val_one`, `val_sub`, `val_zero`, `ind`, `instArchimedean`, `instIsOrderedRing`, `lt_of_mk_lt_mk`, `mk_eq_mk`, `mk_eq_zero`, `mk_le_mk`, `mk_lt_mk`, `mk_ne_zero`, `mk_ratCast`, `ofArchimedean_apply`, `ofArchimedean_inj`, `ofArchimedean_injective`, `ordConnected_preimage_mk`, `le_stdPart_of_le`, `lt_of_lt_stdPart`, `lt_of_stdPart_lt`, `mk_sub_pos_iff`, `mk_sub_stdPart_pos`, `ofArchimedean_stdPart`, `stdPart_add`, `stdPart_add_eq_left`, `stdPart_add_eq_right`, `stdPart_div`, `stdPart_eq`, `stdPart_eq_sInf`, `stdPart_eq_sSup`, `stdPart_eq_zero`, `stdPart_intCast`, `stdPart_inv`, `stdPart_le_of_le`, `stdPart_map_real`, `stdPart_monotoneOn`, `stdPart_mul`, `stdPart_natCast`, `stdPart_neg`, `stdPart_nonneg`, `stdPart_nonpos`, `stdPart_ofNat`, `stdPart_of_mk_ne_zero`, `stdPart_of_mk_nonneg`, `stdPart_one`, `stdPart_ratCast`, `stdPart_real`, `stdPart_sub`, `stdPart_sub_eq_left`, `stdPart_sub_eq_right`, `stdPart_zero`	72
Total	84

ArchimedeanClass

Definitions

Name	Category	Theorems
`FiniteElement` 📖	CompOp	31 math math: `FiniteResidueField.mk_ratCast`, `FiniteElement.instIsStrictOrderedRing`, `FiniteResidueField.ofArchimedean_apply`, `FiniteResidueField.mk_eq_zero`, `FiniteElement.val_add`, `FiniteElement.not_isUnit_iff_mk_pos`, `FiniteElement.mk_le_mk`, `FiniteElement.mk_intCast`, `FiniteElement.val_mul`, `FiniteElement.mk_mul_mk`, `FiniteElement.mk_add_mk`, `FiniteElement.instValuationRing`, `FiniteElement.val_sub`, `FiniteElement.mk_ratCast`, `FiniteResidueField.mk_eq_mk`, `FiniteElement.val_zero`, `FiniteElement.isUnit_iff_mk_eq_zero`, `FiniteElement.instIsDomain`, `FiniteResidueField.mk_le_mk`, `FiniteElement.val_one`, `FiniteElement.mk_zero`, `ofArchimedean_stdPart`, `FiniteElement.mk_neg`, `FiniteResidueField.mk_lt_mk`, `FiniteElement.mk_one`, `FiniteResidueField.ordConnected_preimage_mk`, `stdPart_of_mk_nonneg`, `FiniteElement.mk_lt_mk`, `FiniteElement.mk_natCast`, `FiniteElement.neg_mk`, `FiniteElement.mk_sub_mk`
`FiniteResidueField` 📖	CompOp	13 math math: `FiniteResidueField.mk_ratCast`, `FiniteResidueField.ofArchimedean_apply`, `FiniteResidueField.mk_eq_zero`, `FiniteResidueField.ofArchimedean_inj`, `FiniteResidueField.ofArchimedean_injective`, `FiniteResidueField.mk_eq_mk`, `FiniteResidueField.mk_le_mk`, `FiniteResidueField.instArchimedean`, `ofArchimedean_stdPart`, `FiniteResidueField.mk_lt_mk`, `FiniteResidueField.ordConnected_preimage_mk`, `stdPart_of_mk_nonneg`, `FiniteResidueField.instIsOrderedRing`
`stdPart` 📖	CompOp	36 math math: `stdPart_zero`, `stdPart_of_mk_ne_zero`, `stdPart_eq_sInf`, `Hyperreal.stdPart_coe`, `stdPart_add`, `stdPart_map_real`, `stdPart_eq`, `stdPart_ofNat`, `mk_sub_stdPart_pos`, `stdPart_one`, `stdPart_intCast`, `stdPart_add_eq_right`, `stdPart_monotoneOn`, `stdPart_neg`, `stdPart_sub_eq_right`, `stdPart_natCast`, `ofArchimedean_stdPart`, `stdPart_div`, `stdPart_nonneg`, `stdPart_le_of_le`, `stdPart_sub`, `stdPart_sub_eq_left`, `stdPart_eq_zero`, `mk_sub_pos_iff`, `Hyperreal.stdPart_of_tendsto`, `stdPart_add_eq_left`, `stdPart_mul`, `Hyperreal.stdPart_omega`, `le_stdPart_of_le`, `stdPart_of_mk_nonneg`, `Hyperreal.stdPart_epsilon`, `stdPart_ratCast`, `stdPart_real`, `stdPart_inv`, `stdPart_nonpos`, `stdPart_eq_sSup`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`le_stdPart_of_le` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `DFunLike.coe` `OrderRingHom` `Real` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `OrderRingHom.instFunLike`	`Real.instLE` `stdPart`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `le_imp_le_iff_lt_imp_lt` `lt_of_stdPart_lt`
`lt_of_lt_stdPart` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `Real` `Real.instLT` `stdPart`	`Preorder.toLT` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `OrderRingHom.instFunLike`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `sub_lt_sub_iff_right` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `map_sub` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `OrderRingHom.instRingHomClass` `lt_of_mk_lt_mk_of_nonpos` `IsStrictOrderedRing.toIsOrderedRing` `mk_map_of_archimedean'` `Real.instArchimedean` `sub_eq_zero` `LT.lt.ne` `mk_sub_pos_iff` `AddGroup.toOrderedSub` `zero_add` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `OrderRingHom.toRingHom_eq_coe` `OrderRingHom.monotone'` `LT.lt.le`
`lt_of_stdPart_lt` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `Real` `Real.instLT` `stdPart`	`Preorder.toLT` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `OrderRingHom.instFunLike`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `neg_lt_neg_iff` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `OrderRingHom.instRingHomClass` `lt_of_lt_stdPart` `mk_neg` `stdPart_neg` `Real.instIsOrderedAddMonoid`
`mk_sub_pos_iff` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`Preorder.toLT` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `OrderRingHom` `Real` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `OrderRingHom.instFunLike` `stdPart`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mk_map_nonneg_of_archimedean` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `FiniteResidueField.mk_eq_zero` `map_sub` `RingHomClass.toAddMonoidHomClass` `OrderRingHom.instRingHomClass` `FiniteResidueField.ofArchimedean_apply` `ofArchimedean_stdPart` `sub_eq_zero`
`mk_sub_stdPart_pos` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`Preorder.toLT` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `DFunLike.coe` `OrderRingHom` `Real` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `OrderRingHom.instFunLike` `stdPart`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mk_sub_pos_iff`
`ofArchimedean_stdPart` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`DFunLike.coe` `OrderRingHom` `Real` `FiniteResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Real.commRing` `Real.linearOrder` `FiniteResidueField.instField` `FiniteResidueField.instLinearOrder` `OrderRingHom.instFunLike` `FiniteResidueField.ofArchimedean` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `stdPart` `FiniteElement` `FiniteElement.instCommRing` `FiniteElement.instLinearOrder`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `FiniteResidueField.instArchimedean` `OrderRingHom.comp_apply` `OrderRingHom.comp_assoc` `OrderRingHom.apply_eq_self` `FiniteResidueField.instIsOrderedRing`
`stdPart_add` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`stdPart` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Real` `Real.instAdd`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `FiniteResidueField.instArchimedean` `NonUnitalSubsemiringClass.toAddSubmonoidClass` `SubringClass.toSubsemiringClass` `map_add` `AddMonoidHomClass.toAddHomClass` `RingHomClass.toAddMonoidHomClass` `OrderRingHom.instRingHomClass`
`stdPart_add_eq_left` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`stdPart` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `add_comm` `stdPart_add_eq_right`
`stdPart_add_eq_right` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`stdPart` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `le_or_gt` `stdPart_add` `LT.lt.le` `stdPart_of_mk_ne_zero` `LT.lt.ne'` `zero_add` `LT.lt.ne` `mk_add_eq_mk_right` `LT.lt.trans`
`stdPart_div` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `instNeg`	`stdPart` `DivInvMonoid.toDiv` `DivisionRing.toDivInvMonoid` `Real` `Real.instDivInvMonoid`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `div_eq_mul_inv` `stdPart_mul` `mk_inv` `stdPart_inv`
`stdPart_eq` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `OrderRingHom` `Real` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `OrderRingHom.instFunLike`	`stdPart`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mk_nonneg_of_le_of_le_of_archimedean` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `Real.instZeroLEOneClass` `NeZero.charZero_one` `IsStrictOrderedRing.toCharZero` `contravariant_lt_of_covariant_le` `lt_trichotomy` `exists_between` `LinearOrderedSemiField.toDenselyOrdered` `PosMulReflectLE.toPosMulReflectLT` `PosMulStrictMono.toPosMulReflectLE` `IsStrictOrderedRing.toPosMulStrictMono` `LE.le.not_gt` `le_stdPart_of_le` `stdPart_le_of_le`
`stdPart_eq_sInf` 📖	mathematical	—	`stdPart` `InfSet.sInf` `Real` `Real.instInfSet` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `OrderRingHom.instFunLike`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `le_or_gt` `exists_int_lt_of_mk_nonneg` `exists_int_gt_of_mk_nonneg` `map_intCast` `OrderRingHom.instRingHomClass` `LE.le.not_gt` `OrderRingHom.monotone'` `LT.lt.le` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `RingHom.instRingHomClass` `OrderRingHom.toRingHom_eq_coe` `LT.lt.trans` `stdPart_eq` `notMem_of_lt_csInf` `csInf_lt_iff` `LE.le.trans` `stdPart_of_mk_ne_zero` `LT.lt.ne` `IsStrictOrderedRing.toIsOrderedRing` `LT.lt.trans_le` `mk_map_nonneg_of_archimedean` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `Set.eq_empty_iff_forall_notMem` `LT.lt.not_gt` `lt_of_mk_lt_mk_of_nonneg` `Real.sInf_empty` `Set.eq_univ_iff_forall` `lt_of_mk_lt_mk_of_nonpos` `Real.sInf_univ`
`stdPart_eq_sSup` 📖	mathematical	—	`stdPart` `SupSet.sSup` `Real` `Real.instSupSet` `setOf` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `OrderRingHom.instFunLike`	—	`stdPart_neg` `stdPart_eq_sInf` `Real.sInf_neg` `Set.ext` `map_neg` `DistribMulActionSemiHomClass.toAddMonoidHomClass` `IsStrictOrderedRing.toCharZero` `Real.instIsStrictOrderedRing` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `SemilinearMapClass.distribMulActionSemiHomClass` `RingHomClass.toLinearMapClassNNRat` `OrderRingHom.instRingHomClass` `IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add`
`stdPart_eq_zero` 📖	mathematical	—	`stdPart` `Real` `Real.instZero`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Mathlib.Tactic.Contrapose.contrapose₃` `FiniteResidueField.instIsOrderedRing` `FiniteResidueField.instArchimedean` `Eq.ge` `stdPart_of_mk_nonneg` `map_ne_zero` `Real.instNontrivial` `RingHomClass.toMonoidWithZeroHomClass` `OrderRingHom.instRingHomClass` `FiniteResidueField.mk_ne_zero` `Ne.lt_or_gt` `LT.lt.not_ge` `LT.lt.le` `OrderRingHom.comp_apply` `FiniteResidueField.mk_eq_zero` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass`
`stdPart_intCast` 📖	mathematical	—	`stdPart` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instIntCast`	—	`stdPart.congr_simp` `Rat.cast_intCast` `stdPart_ratCast`
`stdPart_inv` 📖	mathematical	—	`stdPart` `InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `DivisionCommMonoid.toDivisionMonoid` `CommGroupWithZero.toDivisionCommMonoid` `Semifield.toCommGroupWithZero` `Field.toSemifield` `Real` `Real.instInv`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `eq_or_ne` `neg_zero` `FiniteResidueField.instArchimedean` `Eq.ge` `eq_inv_of_mul_eq_one_left` `FiniteElement.ext` `inv_mul_cancel₀` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `OrderRingHom.instRingHomClass` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `stdPart_of_mk_ne_zero` `mk_inv` `neg_ne_zero` `inv_zero`
`stdPart_le_of_le` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `DFunLike.coe` `OrderRingHom` `Real` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `OrderRingHom.instFunLike`	`Real.instLE` `stdPart`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `le_imp_le_iff_lt_imp_lt` `lt_of_lt_stdPart`
`stdPart_map_real` 📖	mathematical	—	`stdPart` `DFunLike.coe` `OrderRingHom` `Real` `Semiring.toNonAssocSemiring` `Real.semiring` `Real.instPreorder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `OrderRingHom.instFunLike`	—	`FiniteResidueField.instArchimedean` `Real.instIsStrictOrderedRing` `Real.instArchimedean` `Real.ringHom_apply` `OrderRingHom.instRingHomClass`
`stdPart_monotoneOn` 📖	mathematical	—	`MonotoneOn` `Real` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Real.instPreorder` `stdPart` `setOf` `ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Preorder.toLE` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `FiniteResidueField.instArchimedean` `OrderRingHom.monotone'`
`stdPart_mul` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`stdPart` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `Real` `Real.instMul`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `FiniteResidueField.instArchimedean` `NonUnitalSubsemiringClass.mulMemClass` `SubringClass.toSubsemiringClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `OrderRingHom.instRingHomClass`
`stdPart_natCast` 📖	mathematical	—	`stdPart` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instNatCast`	—	`stdPart.congr_simp` `Int.cast_natCast` `stdPart_intCast`
`stdPart_neg` 📖	mathematical	—	`stdPart` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instNeg`	—	`FiniteResidueField.instArchimedean` `mk_neg` `map_neg` `RingHomClass.toAddMonoidHomClass` `OrderRingHom.instRingHomClass` `neg_zero`
`stdPart_nonneg` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Real` `Real.instLE` `Real.instZero` `stdPart`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `eq_or_ne` `FiniteResidueField.instArchimedean` `Eq.ge` `map_nonneg` `OrderRingHom.instOrderHomClass` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `OrderRingHom.instRingHomClass` `stdPart_of_mk_ne_zero` `le_refl`
`stdPart_nonpos` 📖	mathematical	`Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	`Real` `Real.instLE` `stdPart` `Real.instZero`	—	`stdPart_neg` `IsOrderedAddMonoid.toAddLeftMono` `Real.instIsOrderedAddMonoid` `stdPart_nonneg` `neg_nonneg` `IsOrderedRing.toIsOrderedAddMonoid`
`stdPart_ofNat` 📖	mathematical	—	`stdPart` `Real` `Real.instNatCast`	—	`stdPart_natCast`
`stdPart_of_mk_ne_zero` 📖	mathematical	—	`stdPart` `Real` `Real.instZero`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `stdPart_eq_zero`
`stdPart_of_mk_nonneg` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`stdPart` `DFunLike.coe` `OrderRingHom` `FiniteResidueField` `Real` `Semiring.toNonAssocSemiring` `FiniteResidueField.instField` `FiniteResidueField.instLinearOrder` `Real.semiring` `Real.instPreorder` `OrderRingHom.instFunLike` `FiniteElement` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `FiniteElement.instCommRing` `FiniteElement.instLinearOrder`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `FiniteResidueField.instArchimedean` `OrderRingHom.comp_apply` `OrderRingHom.subsingleton` `Real.instIsStrictOrderedRing` `Real.instArchimedean`
`stdPart_one` 📖	mathematical	—	`stdPart` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Real` `Real.instOne`	—	`FiniteResidueField.instArchimedean` `map_one` `MonoidHomClass.toOneHomClass` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `OrderRingHom.instRingHomClass`
`stdPart_ratCast` 📖	mathematical	—	`stdPart` `DivisionRing.toRatCast` `Field.toDivisionRing` `Real` `Real.instRatCast`	—	`IsOrderedRing.toIsStrictOrderedRing` `FiniteResidueField.instIsOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `FiniteResidueField.instArchimedean` `mk_ratCast_nonneg` `stdPart_of_mk_nonneg` `FiniteElement.mk_ratCast` `FiniteResidueField.mk_ratCast` `map_ratCast` `OrderRingHom.instRingHomClass`
`stdPart_real` 📖	mathematical	—	`stdPart` `Real` `Real.linearOrder` `Real.instField` `Real.instIsOrderedRing`	—	`stdPart_map_real` `Real.instIsOrderedRing`
`stdPart_sub` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`stdPart` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Real` `Real.instSub`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `sub_eq_add_neg` `stdPart_add` `mk_neg` `stdPart_neg`
`stdPart_sub_eq_left` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`stdPart` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `sub_eq_add_neg` `stdPart_add_eq_left` `mk_neg`
`stdPart_sub_eq_right` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `instLinearOrder` `instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`stdPart` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `Real` `Real.instNeg`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `sub_eq_add_neg` `stdPart_add_eq_right` `stdPart_neg`
`stdPart_zero` 📖	mathematical	—	`stdPart` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Real` `Real.instZero`	—	`FiniteResidueField.instArchimedean` `map_zero` `MonoidWithZeroHomClass.toZeroHomClass` `RingHomClass.toMonoidWithZeroHomClass` `OrderRingHom.instRingHomClass`

ArchimedeanClass.FiniteElement

Definitions

Name	Category	Theorems
`instCommRing` 📖	CompOp	28 math math: `ArchimedeanClass.FiniteResidueField.mk_ratCast`, `instIsStrictOrderedRing`, `ArchimedeanClass.FiniteResidueField.ofArchimedean_apply`, `ArchimedeanClass.FiniteResidueField.mk_eq_zero`, `val_add`, `not_isUnit_iff_mk_pos`, `mk_intCast`, `val_mul`, `mk_mul_mk`, `mk_add_mk`, `instValuationRing`, `val_sub`, `ArchimedeanClass.FiniteResidueField.mk_eq_mk`, `val_zero`, `isUnit_iff_mk_eq_zero`, `instIsDomain`, `ArchimedeanClass.FiniteResidueField.mk_le_mk`, `val_one`, `mk_zero`, `ArchimedeanClass.ofArchimedean_stdPart`, `mk_neg`, `ArchimedeanClass.FiniteResidueField.mk_lt_mk`, `mk_one`, `ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk`, `ArchimedeanClass.stdPart_of_mk_nonneg`, `mk_natCast`, `neg_mk`, `mk_sub_mk`
`instFloorRing` 📖	CompOp	—
`instLinearOrder` 📖	CompOp	12 math math: `ArchimedeanClass.FiniteResidueField.mk_ratCast`, `instIsStrictOrderedRing`, `ArchimedeanClass.FiniteResidueField.ofArchimedean_apply`, `ArchimedeanClass.FiniteResidueField.mk_eq_zero`, `mk_le_mk`, `ArchimedeanClass.FiniteResidueField.mk_eq_mk`, `ArchimedeanClass.FiniteResidueField.mk_le_mk`, `ArchimedeanClass.ofArchimedean_stdPart`, `ArchimedeanClass.FiniteResidueField.mk_lt_mk`, `ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk`, `ArchimedeanClass.stdPart_of_mk_nonneg`, `mk_lt_mk`
`instRatCast` 📖	CompOp	2 math math: `ArchimedeanClass.FiniteResidueField.mk_ratCast`, `mk_ratCast`
`mk` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ext` 📖	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `Ring.toAddCommGroup` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation`	—	—	—
`ext_iff` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `Ring.toAddCommGroup` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation`	—	`ext`
`instIsDomain` 📖	mathematical	—	`IsDomain` `ArchimedeanClass.FiniteElement` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`ValuationSubring.instIsDomainSubtypeMem`
`instIsStrictOrderedRing` 📖	mathematical	—	`IsStrictOrderedRing` `ArchimedeanClass.FiniteElement` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`Subring.toIsStrictOrderedRing` `ValuationSubring.instSubringClass` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`instValuationRing` 📖	mathematical	—	`ValuationRing` `ArchimedeanClass.FiniteElement` `instCommRing` `instIsDomain`	—	`instIsDomain` `ValuationSubring.instValuationRingSubtypeMem`
`isUnit_iff_mk_eq_zero` 📖	mathematical	—	`IsUnit` `ArchimedeanClass.FiniteElement` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation` `ArchimedeanClass.instZero` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `not_iff_not` `not_isUnit_iff_mk_pos` `lt_iff_not_ge` `LE.le.ge_iff_eq'`
`mk_add_mk` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`ArchimedeanClass.FiniteElement` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `instCommRing` `LE.le.trans` `LinearOrder.toMin` `le_min` `ArchimedeanClass.min_le_mk_add`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`mk_intCast` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `ArchimedeanClass.mk_intCast_nonneg` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsDomain.to_noZeroDivisors` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `ArchimedeanClass.FiniteElement` `CommRing.toRing` `instCommRing`	—	`ArchimedeanClass.mk_intCast_nonneg` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`mk_le_mk` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`ArchimedeanClass.FiniteElement` `instLinearOrder`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`mk_lt_mk` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`ArchimedeanClass.FiniteElement` `Preorder.toLT` `instLinearOrder`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`mk_mul_mk` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `AddZero.toZero` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `LinearOrderedAddCommGroupWithTop.toSubNegMonoid` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop`	`ArchimedeanClass.FiniteElement` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `add_nonneg` `IsOrderedAddMonoid.toAddLeftMono` `ArchimedeanClass.instAddCommMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `ArchimedeanClass.instIsOrderedAddMonoid`	—	`IsOrderedRing.toIsOrderedAddMonoid`
`mk_natCast` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `ArchimedeanClass.mk_natCast_nonneg` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `IsDomain.to_noZeroDivisors` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `ArchimedeanClass.FiniteElement` `CommRing.toRing` `instCommRing`	—	`ArchimedeanClass.mk_natCast_nonneg` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`mk_neg` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`ArchimedeanClass.FiniteElement` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CommRing.toRing` `instCommRing`	—	—
`mk_one` 📖	mathematical	—	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `ArchimedeanClass.FiniteElement` `CommRing.toRing` `instCommRing`	—	—
`mk_ratCast` 📖	mathematical	—	`DivisionRing.toRatCast` `Field.toDivisionRing` `ArchimedeanClass.mk_ratCast_nonneg` `ArchimedeanClass.FiniteElement` `instRatCast`	—	`ArchimedeanClass.mk_ratCast_nonneg`
`mk_sub_mk` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `LinearOrder.toPartialOrder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`ArchimedeanClass.FiniteElement` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing` `LE.le.trans` `LinearOrder.toMin` `le_min` `ArchimedeanClass.min_le_mk_sub`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`mk_zero` 📖	mathematical	—	`MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ArchimedeanClass.FiniteElement` `instCommRing`	—	—
`neg_mk` 📖	mathematical	`ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLE` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	`ArchimedeanClass.FiniteElement` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `CommRing.toRing` `instCommRing`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing`
`not_isUnit_iff_mk_pos` 📖	mathematical	—	`IsUnit` `ArchimedeanClass.FiniteElement` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing` `ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `Preorder.toLT` `PartialOrder.toPreorder` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `CommRing.toRing` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation`	—	`Valuation.Integer.not_isUnit_iff_valuation_lt_one`
`val_add` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `Ring.toAddCommGroup` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation` `ArchimedeanClass.FiniteElement` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	—
`val_mul` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `Ring.toAddCommGroup` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation` `ArchimedeanClass.FiniteElement` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	—
`val_one` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `Ring.toAddCommGroup` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation` `ArchimedeanClass.FiniteElement` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `instCommRing` `DivisionRing.toRing` `Field.toDivisionRing`	—	—
`val_sub` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `Ring.toAddCommGroup` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation` `ArchimedeanClass.FiniteElement` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `instCommRing` `DivisionRing.toRing` `Field.toDivisionRing`	—	—
`val_zero` 📖	mathematical	—	`ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `Ring.toAddCommGroup` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation` `ArchimedeanClass.FiniteElement` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	—

ArchimedeanClass.FiniteResidueField

Definitions

Name	Category	Theorems
`instField` 📖	CompOp	13 math math: `mk_ratCast`, `ofArchimedean_apply`, `mk_eq_zero`, `ofArchimedean_inj`, `ofArchimedean_injective`, `mk_eq_mk`, `mk_le_mk`, `instArchimedean`, `ArchimedeanClass.ofArchimedean_stdPart`, `mk_lt_mk`, `ordConnected_preimage_mk`, `ArchimedeanClass.stdPart_of_mk_nonneg`, `instIsOrderedRing`
`instLinearOrder` 📖	CompOp	13 math math: `mk_ratCast`, `ofArchimedean_apply`, `mk_eq_zero`, `ofArchimedean_inj`, `ofArchimedean_injective`, `mk_eq_mk`, `mk_le_mk`, `instArchimedean`, `ArchimedeanClass.ofArchimedean_stdPart`, `mk_lt_mk`, `ordConnected_preimage_mk`, `ArchimedeanClass.stdPart_of_mk_nonneg`, `instIsOrderedRing`
`mk` 📖	CompOp	—
`ofArchimedean` 📖	CompOp	4 math math: `ofArchimedean_apply`, `ofArchimedean_inj`, `ofArchimedean_injective`, `ArchimedeanClass.ofArchimedean_stdPart`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`ind` 📖	—	`DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteElement` `ArchimedeanClass.FiniteResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ArchimedeanClass.FiniteElement.instCommRing` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.FiniteElement.instLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instLinearOrder` `OrderRingHom.instFunLike`	—	—	—
`instArchimedean` 📖	mathematical	—	`Archimedean` `ArchimedeanClass.FiniteResidueField` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instField` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`ind` `le_or_gt` `zero_nsmul` `IsOrderedRing.toIsOrderedAddMonoid` `Eq.le` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mk_ne_zero` `LT.lt.ne'` `OrderRingHom.monotone'` `abs_of_pos` `IsOrderedAddMonoid.toAddLeftMono`
`instIsOrderedRing` 📖	mathematical	—	`IsOrderedRing` `ArchimedeanClass.FiniteResidueField` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder`	—	`ind` `OrderRingHom.monotone'` `add_le_add_left` `covariant_swap_add_of_covariant_add` `IsOrderedAddMonoid.toAddLeftMono` `IsOrderedRing.toIsOrderedAddMonoid` `IsStrictOrderedRing.toIsOrderedRing` `ArchimedeanClass.FiniteElement.instIsStrictOrderedRing` `le_refl` `zero_le_one` `IsStrictOrderedRing.toZeroLEOneClass` `mul_comm`
`lt_of_mk_lt_mk` 📖	—	`ArchimedeanClass.FiniteResidueField` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteElement` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ArchimedeanClass.FiniteElement.instCommRing` `ArchimedeanClass.FiniteElement.instLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `OrderRingHom.instFunLike`	—	—	—
`mk_eq_mk` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteElement` `ArchimedeanClass.FiniteResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ArchimedeanClass.FiniteElement.instCommRing` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.FiniteElement.instLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instLinearOrder` `OrderRingHom.instFunLike` `ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `Preorder.toLT` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup` `Ring.toAddGroupWithOne` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `CommRing.toRing` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `Quotient.eq` `Submodule.quotientRel_def` `IsLocalRing.mem_maximalIdeal` `mem_nonunits_iff` `ArchimedeanClass.FiniteElement.not_isUnit_iff_mk_pos` `SubringClass.addSubgroupClass` `ValuationSubring.instSubringClass` `AddSubgroupClass.coe_sub`
`mk_eq_zero` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteElement` `ArchimedeanClass.FiniteResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ArchimedeanClass.FiniteElement.instCommRing` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.FiniteElement.instLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instLinearOrder` `OrderRingHom.instFunLike` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ArchimedeanClass` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `Preorder.toLT` `ArchimedeanClass.instLinearOrder` `ArchimedeanClass.instZero` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `CommRing.toRing` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `sub_zero`
`mk_le_mk` 📖	mathematical	—	`ArchimedeanClass.FiniteResidueField` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteElement` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ArchimedeanClass.FiniteElement.instCommRing` `ArchimedeanClass.FiniteElement.instLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `OrderRingHom.instFunLike`	—	`ValuationRing.isLocalRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `ArchimedeanClass.FiniteElement.instIsStrictOrderedRing` `ValuationRing.toPreValuationRing` `ArchimedeanClass.FiniteElement.instIsDomain` `ArchimedeanClass.FiniteElement.instValuationRing` `Quotient.eq_iff_equiv`
`mk_lt_mk` 📖	mathematical	—	`ArchimedeanClass.FiniteResidueField` `Preorder.toLT` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `instLinearOrder` `DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteElement` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ArchimedeanClass.FiniteElement.instCommRing` `ArchimedeanClass.FiniteElement.instLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `OrderRingHom.instFunLike`	—	`ValuationRing.isLocalRing` `instNontrivialOfCharZero` `IsStrictOrderedRing.toCharZero` `ArchimedeanClass.FiniteElement.instIsStrictOrderedRing` `ValuationRing.toPreValuationRing` `ArchimedeanClass.FiniteElement.instIsDomain` `ArchimedeanClass.FiniteElement.instValuationRing` `Quotient.eq_iff_equiv`
`mk_ne_zero` 📖	mathematical	—	`Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `IsOrderedRing.toIsOrderedAddMonoid` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ValuationSubring` `SetLike.instMembership` `ValuationSubring.instSetLike` `Valuation.valuationSubring` `Multiplicative` `OrderDual` `ArchimedeanClass` `CommRing.toRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instLinearOrderedCommGroupWithZeroMultiplicativeOrderDualOfLinearOrderedAddCommGroupWithTop` `ArchimedeanClass.instLinearOrderedAddCommGroupWithTop` `DFunLike.coe` `Equiv` `AddValuation` `ArchimedeanClass.instLinearOrderedAddCommMonoidWithTop` `Valuation` `instLinearOrderedCommMonoidWithZeroMultiplicativeOrderDual` `EquivLike.toFunLike` `Equiv.instEquivLike` `AddValuation.toValuation` `ArchimedeanClass.addValuation` `ArchimedeanClass.instZero` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	—	`IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `mk_eq_zero` `not_lt` `LE.le.ge_iff_eq'`
`mk_ratCast` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteElement` `ArchimedeanClass.FiniteResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ArchimedeanClass.FiniteElement.instCommRing` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.FiniteElement.instLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instLinearOrder` `OrderRingHom.instFunLike` `ArchimedeanClass.FiniteElement.instRatCast` `DivisionRing.toRatCast` `Field.toDivisionRing`	—	`ArchimedeanClass.mk_ratCast_nonneg` `mul_left_inj'` `IsCancelMulZero.toIsRightCancelMulZero` `IsDomain.toIsCancelMulZero` `instIsDomain` `Nat.cast_zero` `IsStrictOrderedRing.toCharZero` `IsOrderedRing.toIsStrictOrderedRing` `instIsOrderedRing` `IsDomain.to_noZeroDivisors` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `map_natCast` `OrderRingHom.instRingHomClass` `map_mul` `NonUnitalRingHomClass.toMulHomClass` `RingHomClass.toNonUnitalRingHomClass` `ArchimedeanClass.mk_natCast_nonneg` `ArchimedeanClass.FiniteElement.mk_natCast` `add_nonneg` `IsOrderedRing.toIsOrderedAddMonoid` `IsOrderedAddMonoid.toAddLeftMono` `ArchimedeanClass.instIsOrderedAddMonoid` `Rat.cast_div` `Rat.cast_intCast` `Rat.cast_natCast` `IsUnit.div_mul_cancel` `map_intCast`
`ofArchimedean_apply` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instLinearOrder` `OrderRingHom.instFunLike` `ofArchimedean` `ArchimedeanClass.FiniteElement` `ArchimedeanClass.FiniteElement.instCommRing` `ArchimedeanClass.FiniteElement.instLinearOrder` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `ArchimedeanClass.mk_map_nonneg_of_archimedean` `IsOrderedRing.toIsStrictOrderedRing` `DivisionRing.toRing` `Field.toDivisionRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `DivisionRing.isSimpleRing`	—	—
`ofArchimedean_inj` 📖	mathematical	—	`DFunLike.coe` `OrderRingHom` `ArchimedeanClass.FiniteResidueField` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instLinearOrder` `OrderRingHom.instFunLike` `ofArchimedean`	—	`ofArchimedean_injective`
`ofArchimedean_injective` 📖	mathematical	—	`ArchimedeanClass.FiniteResidueField` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instLinearOrder` `OrderRingHom.instFunLike` `ofArchimedean`	—	`injective_iff_map_eq_zero` `RingHomClass.toAddMonoidHomClass` `OrderRingHom.instRingHomClass` `Mathlib.Tactic.Contrapose.contrapose₁` `ArchimedeanClass.mk_map_nonneg_of_archimedean` `IsOrderedRing.toIsStrictOrderedRing` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsSimpleRing.instNontrivial` `DivisionRing.isSimpleRing` `ofArchimedean_apply` `IsOrderedRing.toIsOrderedAddMonoid` `mk_ne_zero` `ArchimedeanClass.mk_map_of_archimedean'`
`ordConnected_preimage_mk` 📖	mathematical	—	`Set.OrdConnected` `ArchimedeanClass.FiniteElement` `PartialOrder.toPreorder` `SemilatticeInf.toPartialOrder` `Lattice.toSemilatticeInf` `DistribLattice.toLattice` `instDistribLatticeOfLinearOrder` `ArchimedeanClass.FiniteElement.instLinearOrder` `Set.preimage` `ArchimedeanClass.FiniteResidueField` `DFunLike.coe` `OrderRingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ArchimedeanClass.FiniteElement.instCommRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instLinearOrder` `OrderRingHom.instFunLike` `Set` `Set.instSingletonSet`	—	—

---

← Back to Index