Ring

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

Statistics

Metric	Count
Definitions Ring, Ring, OrderRingHom, comp, copy, id, instFunLike, instInhabited, instPartialOrder, instPreorder, toOrderAddMonoidHom, toOrderMonoidWithZeroHom, toRingHom, toOrderRingHom, OrderRingIso, symm_apply, instEquivLike, instInhabited, refl, toOrderIso, toOrderRingHom, toRingEquiv, trans, toOrderRingIso, instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass, instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass, «term_→+*o_», «term_≃+*o_»	28
Theorems cancel_left, cancel_right, coe_coe_orderAddMonoidHom, coe_coe_orderMonoidWithZeroHom, coe_coe_ringHom, coe_comp, coe_copy, coe_id, coe_orderAddMonoidHom_apply, coe_orderAddMonoidHom_id, coe_orderMonoidWithZeroHom_apply, coe_orderMonoidWithZeroHom_id, coe_ringHom_apply, coe_ringHom_id, comp_apply, comp_assoc, comp_id, copy_eq, ext, ext_iff, id_apply, id_comp, instOrderHomClass, instRingHomClass, monotone', toFun_eq_coe, toOrderAddMonoidHom_eq_coe, toOrderMonoidWithZeroHom_eq_coe, toRingHom_eq_coe, apply_symm_apply, coe_mk, coe_orderIso_refl, coe_ringEquiv_refl, coe_toOrderIso, coe_toOrderRingHom, coe_toOrderRingHom_refl, coe_toRingEquiv, ext, ext_iff, instOrderIsoClass, instRingEquivClass, lt_symm_apply, map_le_map_iff', mk_coe, refl_apply, self_trans_symm, symm_apply_apply, symm_apply_lt, symm_bijective, symm_symm, symm_trans_self, toFun_eq_coe, toOrderIso_eq_coe, toOrderRingHom_eq_coe, toOrderRingHom_injective, toRingEquiv_eq_coe, trans_apply, trans_toRingEquiv, trans_toRingEquiv_aux	59
Total	87

Algebra.Extension

Definitions

Name	Category	Theorems
Ring 📖	CompOp	98 math math: Algebra.Presentation.differentials.comm₁₂_single, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, ofSurjective_Ring, H1Cotangent.equiv_apply, Algebra.Generators.cotangentSpaceBasis_apply, Algebra.Presentation.differentials.comm₂₃, Cotangent.val_sub, formallySmooth_iff_split_injection, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, CotangentSpace.map_id, Algebra.Presentation.differentials.hom₁_single, Algebra.Generators.exists_presentation_of_basis_cotangent, lTensor_cotangentComplex_eq_cotangentComplexBaseChange, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, Cotangent.val_mk, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, subsingleton_h1Cotangent, Algebra.Generators.exists_presentation_of_free_cotangent, CotangentSpace.map_tmul, H1Cotangent.val_zero, Cotangent.val_smul''', Cotangent.val_add, instIsScalarTowerRing, algebraMap_surjective, Algebra.Generators.CotangentSpace.compEquiv_symm_zero, Algebra.Generators.cotangentSpaceBasis_repr_tmul, isScalarTower, Hom.sub_one_tmul, Algebra.Generators.H1Cotangent.δAux_toAlgHom, Hom.id_toRingHom, CotangentSpace.map_toInfinitesimal_bijective, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, Cotangent.mk_eq_zero_iff, CotangentSpace.map_sub_map, Hom.toRingHom_algebraMap, CotangentSpace.map_cotangentComplex, cotangentComplexBaseChange_eq_lTensor_cotangentComplex, Algebra.Generators.H1Cotangent.δAux_ofComp, Algebra.Presentation.differentials.comm₂₃', Cotangent.val_smul', contangentEquiv_tmul, ker_infinitesimal, Algebra.Generators.cMulXSubOneCotangent_eq, h1Cotangentι_ext_iff, Algebra.Generators.toKaehler_tmul_D, H1Cotangent.val_add, H1Cotangent.val_smul, Algebra.Presentation.differentials.comm₁₂, Cotangent.mk_eq_mk_iff_sub_mem, instIsScalarTowerRing_1, toKaehler_surjective, Algebra.Generators.disjoint_ker_toKaehler_of_linearIndependent, Cotangent.mk_surjective, Algebra.Generators.CotangentSpace.exact, Hom.subToKer_apply_coe, Algebra.Generators.repr_CotangentSpaceMap, H1Cotangent.map_apply_coe, Algebra.Generators.toKaehler_cotangentSpaceBasis, Cotangent.val_smul, Hom.algebraMap_toRingHom, Algebra.Generators.CotangentSpace.compEquiv_symm_inr, algebraMap_σ, Hom.sub_aux, h1Cotangentι_apply, cotangentComplex_injective_iff, σ_injective, Algebra.Generators.cotangentRestrict_mk, Algebra.Generators.CotangentSpace.map_toComp_injective, Cotangent.val_zero, Algebra.Generators.toExtension_Ring, Hom.sub_tmul, Cotangent.of_add, Algebra.SubmersivePresentation.sectionCotangent_comp, σ_smul, Algebra.SubmersivePresentation.sectionCotangent_zero_of_notMem_range, Algebra.Generators.instFreeCotangentSpaceToExtension, Algebra.Generators.CotangentSpace.fst_compEquiv_apply, instIsScalarTowerRing_2, self_Ring, Algebra.SubmersivePresentation.cotangentComplex_injective, Algebra.SubmersivePresentation.basisCotangent_apply, Cotangent.map_mk, CotangentSpace.map_comp, exact_cotangentComplex_toKaehler, Algebra.Generators.CotangentSpace.map_ofComp_surjective, Algebra.Generators.H1Cotangent.map_comp_cotangentComplex_baseChange, Algebra.Generators.CotangentSpace.fst_compEquiv, CotangentSpace.map_comp_apply, Algebra.Generators.H1Cotangent.equiv_apply, CotangentSpace.map_comp_cotangentComplex, Cotangent.ker_mk, Hom.comp_toRingHom, Hom.toAlgHom_id, Hom.toAlgHom_apply, Cotangent.map_sub_map, Cotangent.of_zero, cotangentComplex_mk, Cotangent.val_smul''

Algebra.Generators

Definitions

Name	Category	Theorems
Ring 📖	CompOp	70 math math: Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, H1Cotangent.δAux_mul, cotangentSpaceBasis_apply, toAlgHom_ofComp_localizationAway, Algebra.Presentation.localizationAway_relation, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, defaultHom_val, compLocalizationAwayAlgHom_toAlgHom_toComp, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, algebraMap_surjective, Algebra.Presentation.quotientEquiv_symm, H1Cotangent.δAux_C, map_toComp_ker, Hom.toExtensionHom_toAlgHom_apply, ofComp_val, algebraMap_apply, compLocalizationAwayAlgHom_X_inl, map_ofComp_ker, Algebra.SubmersivePresentation.ofSubsingleton_relation, Algebra.SubmersivePresentation.jacobianRelations_spec, H1Cotangent.δAux_monomial, toAlgHom_ofComp_surjective, Hom.algebraMap_toAlgHom', cotangentSpaceBasis_repr_tmul, H1Cotangent.δAux_toAlgHom, sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Algebra.Presentation.span_range_relation_eq_ker, Hom.toAlgHom_X, Algebra.Presentation.comp_relation, instIsScalarTowerRing, H1Cotangent.δAux_ofComp, toAlgHom_ofComp_rename, ker_localizationAway, Algebra.Presentation.fg_ker, σ_smul, Algebra.Presentation.relation_mem_ker, Hom.toExtensionHom_toRingHom, MvPolynomial.universalFactorizationMapPresentation_relation, σ_injective, toKaehler_tmul_D, Hom.toAlgHom_C, Hom.toAlgHom_comp_apply, toComp_toAlgHom_monomial, H1Cotangent.δAux_X, ofComp_kerCompPreimage, Hom.equivAlgHom_symm_apply_val, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, ker_comp_eq_sup, ofComp_toAlgHom_monomial_sumElim, cotangentRestrict_mk, H1Cotangent.δ_eq_δAux, Hom.toAlgHom_id, Hom.comp_val, compLocalizationAwayAlgHom_relation_eq_zero, toExtension_Ring, Algebra.Presentation.HasCoeffs.relation_mem_range_map, fg_ker_of_finitePresentation, Hom.toAlgHom_monomial, Algebra.Presentation.quotientEquiv_mk, StandardEtalePresentation.toPresentation_relation, Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, Hom.algebraMap_toAlgHom, Algebra.Presentation.instFinitePresentationQuotientOfFinite, H1Cotangent.equiv_apply, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, Algebra.PreSubmersivePresentation.baseChange_ring, Algebra.Presentation.mem_ker_naive, Hom.equivAlgHom_apply_coe, C_mul_X_sub_one_mem_ker

OrderRingHom

Definitions

Name	Category	Theorems
comp 📖	CompOp	7 math math: comp_id, cancel_right, coe_comp, cancel_left, comp_assoc, comp_apply, id_comp
copy 📖	CompOp	2 math math: copy_eq, coe_copy
id 📖	CompOp	9 math math: eq_id, comp_id, coe_orderAddMonoidHom_id, coe_orderMonoidWithZeroHom_id, coe_id, coe_ringHom_id, OrderRingIso.coe_toOrderRingHom_refl, id_apply, id_comp
instFunLike 📖	CompOp	93 math math: coe_orderAddMonoidHom_apply, Cardinal.natCast_lt_toENat_iff, ArchimedeanClass.FiniteResidueField.mk_ratCast, Subring.orderedSubtype_coe, Set.toENat_cardinalMk_subtype, Cardinal.toENat_eq_natCast_iff, Cardinal.toENat_ofENat, Module.length_of_free, ArchimedeanClass.FiniteResidueField.ofArchimedean_apply, ArchimedeanClass.FiniteResidueField.mk_eq_zero, OrderRingIso.coe_toOrderRingHom, Submodule.spanRank_toENat_eq_iInf_encard, Cardinal.toENat_eq_zero, apply_eq_self, Cardinal.toENat_eq_ofNat, coe_coe_ringHom, coe_orderAddMonoidHom_id, Cardinal.toENat_lt_natCast_iff, Cardinal.toENat_lift, Cardinal.toENat_le_ofNat, ArchimedeanClass.stdPart_eq_sInf, ArchimedeanClass.mk_map_nonneg_of_archimedean, ArchimedeanClass.FiniteResidueField.ofArchimedean_inj, coe_comp, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, ArchimedeanClass.stdPart_map_real, ArchimedeanClass.lt_of_pos_of_archimedean, ArchimedeanClass.mk_sub_stdPart_pos, instOrderHomClass, ArchimedeanClass.FiniteResidueField.ofArchimedean_injective, LinearOrderedField.inducedOrderRingHom_toFun, ext_iff, coe_orderMonoidWithZeroHom_id, ArchimedeanClass.lt_of_lt_stdPart, coe_coe_orderMonoidWithZeroHom, toOrderMonoidWithZeroHom_eq_coe, toFun_eq_coe, coe_id, Cardinal.toNat_toENat, ArchimedeanClass.FiniteResidueField.mk_eq_mk, ArchimedeanClass.lt_of_stdPart_lt, toOrderAddMonoidHom_eq_coe, toENat_rank_span_set, instRingHomClass, Cardinal.toENat_strictMonoOn, coe_ringHom_id, Submodule.spanRank_toENat_eq_iInf_finset_card, coe_coe_orderAddMonoidHom, Cardinal.continuum_toENat, ArchimedeanClass.FiniteResidueField.mk_le_mk, coe_ringHom_apply, toRingHom_eq_coe, Cardinal.toENat_le_iff_of_le_aleph0, Cardinal.toENat_eq_top, ArchimedeanClass.ofArchimedean_stdPart, Cardinal.toENat_le_natCast_iff, Set.toENat_cardinalMk, Cardinal.enat_gc, ArchimedeanClass.lt_of_neg_of_archimedean, ArchimedeanClass.mk_le_mk_add_of_archimedean, Cardinal.toENat_le_nat, ArchimedeanClass.mk_sub_pos_iff, coe_orderMonoidWithZeroHom_apply, ArchimedeanClass.mk_le_add_mk_of_archimedean, ArchimedeanClass.FiniteResidueField.mk_lt_mk, Cardinal.toENat_comp_ofENat, Cardinal.toENat_le_iff_of_lt_aleph0, ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk, Cardinal.ofENat_toENat_le, Cardinal.toENat_le_one, Cardinal.toENat_injOn, LinearIndepOn.encard_le_toENat_rank, Cardinal.toENat_eq_nat, Cardinal.ofENat_toENat_eq_self, Cardinal.ofENat_toENat, id_apply, Cardinal.aleph_toENat, comp_apply, Cardinal.toENat_eq_iff_of_le_aleph0, ArchimedeanClass.stdPart_of_mk_nonneg, Ideal.height_le_spanRank_toENat, Cardinal.natCast_eq_toENat_iff, Cardinal.toENat_nat, Matroid.toENat_cRank_eq, ArchimedeanClass.mk_map_of_archimedean', Cardinal.natCast_le_toENat_iff, Module.length_eq_rank, Cardinal.toENat_lt_top, Cardinal.toENat_congr, Matroid.toENat_cRk_eq, Cardinal.toENat_eq_one, ArchimedeanClass.stdPart_eq_sSup, Hyperreal.coeRingHom_toFun
instInhabited 📖	CompOp	—
instPartialOrder 📖	CompOp	—
instPreorder 📖	CompOp	—
toOrderAddMonoidHom 📖	CompOp	1 math math: toOrderAddMonoidHom_eq_coe
toOrderMonoidWithZeroHom 📖	CompOp	1 math math: toOrderMonoidWithZeroHom_eq_coe
toRingHom 📖	CompOp	3 math math: toFun_eq_coe, monotone', toRingHom_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cancel_left 📖	mathematical	DFunLike.coe OrderRingHom instFunLike	comp	—	ext comp_apply
cancel_right 📖	mathematical	DFunLike.coe OrderRingHom instFunLike	comp	—	ext Function.Surjective.forall DFunLike.ext_iff
coe_coe_orderAddMonoidHom 📖	mathematical	—	DFunLike.coe OrderAddMonoidHom AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne OrderAddMonoidHom.instFunLike OrderMonoidHomClass.toOrderAddMonoidHom OrderRingHom instFunLike instOrderHomClass RingHomClass.toAddMonoidHomClass instRingHomClass	—	instOrderHomClass RingHomClass.toAddMonoidHomClass instRingHomClass
coe_coe_orderMonoidWithZeroHom 📖	mathematical	—	DFunLike.coe OrderMonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass OrderMonoidWithZeroHom.instFunLike OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom OrderRingHom instFunLike instOrderHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass	—	instOrderHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass
coe_coe_ringHom 📖	mathematical	—	DFunLike.coe RingHom RingHom.instFunLike RingHomClass.toRingHom OrderRingHom instFunLike instRingHomClass	—	instRingHomClass
coe_comp 📖	mathematical	—	DFunLike.coe OrderRingHom instFunLike comp	—	—
coe_copy 📖	mathematical	DFunLike.coe OrderRingHom instFunLike	copy	—	—
coe_id 📖	mathematical	—	DFunLike.coe OrderRingHom instFunLike id	—	—
coe_orderAddMonoidHom_apply 📖	mathematical	—	DFunLike.coe OrderAddMonoidHom AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne OrderAddMonoidHom.instFunLike OrderMonoidHomClass.toOrderAddMonoidHom OrderRingHom instFunLike instOrderHomClass RingHomClass.toAddMonoidHomClass instRingHomClass	—	instOrderHomClass RingHomClass.toAddMonoidHomClass instRingHomClass
coe_orderAddMonoidHom_id 📖	mathematical	—	OrderMonoidHomClass.toOrderAddMonoidHom OrderRingHom AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instFunLike instOrderHomClass RingHomClass.toAddMonoidHomClass instRingHomClass id OrderAddMonoidHom.id	—	instOrderHomClass RingHomClass.toAddMonoidHomClass instRingHomClass
coe_orderMonoidWithZeroHom_apply 📖	mathematical	—	DFunLike.coe OrderMonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass OrderMonoidWithZeroHom.instFunLike OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom OrderRingHom instFunLike instOrderHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass	—	instOrderHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass
coe_orderMonoidWithZeroHom_id 📖	mathematical	—	OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom OrderRingHom NonAssocSemiring.toMulZeroOneClass instFunLike instOrderHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass id OrderMonoidWithZeroHom.id	—	instOrderHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass
coe_ringHom_apply 📖	mathematical	—	DFunLike.coe RingHom RingHom.instFunLike RingHomClass.toRingHom OrderRingHom instFunLike instRingHomClass	—	instRingHomClass
coe_ringHom_id 📖	mathematical	—	RingHomClass.toRingHom OrderRingHom instFunLike instRingHomClass id RingHom.id	—	instRingHomClass
comp_apply 📖	mathematical	—	DFunLike.coe OrderRingHom instFunLike comp	—	—
comp_assoc 📖	mathematical	—	comp	—	—
comp_id 📖	mathematical	—	comp id	—	—
copy_eq 📖	mathematical	DFunLike.coe OrderRingHom instFunLike	copy	—	DFunLike.ext'
ext 📖	—	DFunLike.coe OrderRingHom instFunLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe OrderRingHom instFunLike	—	ext
id_apply 📖	mathematical	—	DFunLike.coe OrderRingHom instFunLike id	—	—
id_comp 📖	mathematical	—	comp id	—	—
instOrderHomClass 📖	mathematical	—	OrderHomClass OrderRingHom Preorder.toLE instFunLike	—	monotone'
instRingHomClass 📖	mathematical	—	RingHomClass OrderRingHom instFunLike	—	MonoidHom.map_mul' OneHom.map_one' RingHom.map_add' RingHom.map_zero'
monotone' 📖	mathematical	—	Monotone OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.toOneHom RingHom.toMonoidHom toRingHom	—	—
toFun_eq_coe 📖	mathematical	—	OneHom.toFun MulOne.toOne MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MonoidHom.toOneHom RingHom.toMonoidHom toRingHom DFunLike.coe OrderRingHom instFunLike	—	—
toOrderAddMonoidHom_eq_coe 📖	mathematical	—	toOrderAddMonoidHom OrderMonoidHomClass.toOrderAddMonoidHom OrderRingHom AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne instFunLike instOrderHomClass RingHomClass.toAddMonoidHomClass instRingHomClass	—	—
toOrderMonoidWithZeroHom_eq_coe 📖	mathematical	—	toOrderMonoidWithZeroHom OrderMonoidWithZeroHomClass.toOrderMonoidWithZeroHom OrderRingHom NonAssocSemiring.toMulZeroOneClass instFunLike instOrderHomClass RingHomClass.toMonoidWithZeroHomClass instRingHomClass	—	—
toRingHom_eq_coe 📖	mathematical	—	toRingHom RingHomClass.toRingHom OrderRingHom instFunLike instRingHomClass	—	RingHom.ext instRingHomClass

OrderRingHomClass

Definitions

Name	Category	Theorems
toOrderRingHom 📖	CompOp	3 math math: OrderRingIso.coe_toOrderRingHom, OrderRingIso.coe_toOrderRingHom_refl, OrderRingIso.toOrderRingHom_eq_coe

OrderRingIso

Definitions

Name	Category	Theorems
instEquivLike 📖	CompOp	27 math math: ext_iff, trans_toRingEquiv_aux, apply_symm_apply, Valuation.IsEquiv.orderRingIso_apply, coe_toOrderRingHom, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, toRingEquiv_eq_coe, coe_ringEquiv_refl, trans_apply, coe_mk, symm_apply_apply, toOrderIso_eq_coe, lt_symm_apply, apply_eq_self, coe_toOrderRingHom_refl, LinearOrderedField.coe_inducedOrderRingIso, toOrderRingHom_eq_coe, refl_apply, instRingEquivClass, symm_apply_lt, instOrderIsoClass, coe_toOrderIso, coe_toRingEquiv, toFun_eq_coe, coe_orderIso_refl, Valuation.IsEquiv.orderRingIso_symm_apply
instInhabited 📖	CompOp	—
refl 📖	CompOp	8 math math: LinearOrderedField.inducedOrderRingIso_self, eq_refl, coe_ringEquiv_refl, coe_toOrderRingHom_refl, self_trans_symm, symm_trans_self, refl_apply, coe_orderIso_refl
toOrderIso 📖	CompOp	1 math math: toOrderIso_eq_coe
toOrderRingHom 📖	CompOp	2 math math: toOrderRingHom_injective, toOrderRingHom_eq_coe
toRingEquiv 📖	CompOp	5 math math: trans_toRingEquiv_aux, toRingEquiv_eq_coe, trans_toRingEquiv, map_le_map_iff', toFun_eq_coe
trans 📖	CompOp	5 math math: trans_toRingEquiv_aux, trans_apply, trans_toRingEquiv, self_trans_symm, symm_trans_self

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_symm_apply 📖	mathematical	—	DFunLike.coe OrderRingIso EquivLike.toFunLike instEquivLike symm	—	RingEquiv.apply_symm_apply
coe_mk 📖	mathematical	Equiv.toFun RingEquiv.toEquiv	DFunLike.coe OrderRingIso EquivLike.toFunLike instEquivLike RingEquiv RingEquiv.instEquivLike	—	—
coe_orderIso_refl 📖	mathematical	—	OrderIsoClass.toOrderIso OrderRingIso instEquivLike instOrderIsoClass refl OrderIso.refl	—	instOrderIsoClass
coe_ringEquiv_refl 📖	mathematical	—	RingEquivClass.toRingEquiv OrderRingIso instEquivLike instRingEquivClass refl RingEquiv.refl	—	instRingEquivClass
coe_toOrderIso 📖	mathematical	—	DFunLike.coe OrderIso instFunLikeOrderIso OrderIsoClass.toOrderIso OrderRingIso instEquivLike instOrderIsoClass EquivLike.toFunLike	—	instOrderIsoClass
coe_toOrderRingHom 📖	mathematical	—	DFunLike.coe OrderRingHom OrderRingHom.instFunLike OrderRingHomClass.toOrderRingHom OrderRingIso Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd Preorder.toLE EquivLike.toFunLike instEquivLike OrderIsoClass.toOrderHomClass instOrderIsoClass RingEquivClass.toRingHomClass instRingEquivClass	—	OrderIsoClass.toOrderHomClass instOrderIsoClass RingEquivClass.toRingHomClass instRingEquivClass
coe_toOrderRingHom_refl 📖	mathematical	—	OrderRingHomClass.toOrderRingHom OrderRingIso Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd Preorder.toLE EquivLike.toFunLike instEquivLike OrderIsoClass.toOrderHomClass instOrderIsoClass RingEquivClass.toRingHomClass instRingEquivClass refl OrderRingHom.id	—	OrderIsoClass.toOrderHomClass instOrderIsoClass RingEquivClass.toRingHomClass instRingEquivClass
coe_toRingEquiv 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike RingEquiv.instEquivLike RingEquivClass.toRingEquiv OrderRingIso instEquivLike instRingEquivClass	—	instRingEquivClass
ext 📖	—	DFunLike.coe OrderRingIso EquivLike.toFunLike instEquivLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe OrderRingIso EquivLike.toFunLike instEquivLike	—	ext
instOrderIsoClass 📖	mathematical	—	OrderIsoClass OrderRingIso instEquivLike	—	map_le_map_iff'
instRingEquivClass 📖	mathematical	—	RingEquivClass OrderRingIso instEquivLike	—	RingEquiv.map_mul' RingEquiv.map_add'
lt_symm_apply 📖	mathematical	—	Preorder.toLT DFunLike.coe OrderRingIso Preorder.toLE EquivLike.toFunLike instEquivLike symm	—	instOrderIsoClass toOrderIso_eq_coe OrderIso.lt_symm_apply
map_le_map_iff' 📖	mathematical	—	Equiv.toFun RingEquiv.toEquiv toRingEquiv	—	—
mk_coe 📖	—	Equiv.toFun RingEquiv.toEquiv RingEquivClass.toRingEquiv OrderRingIso instEquivLike instRingEquivClass	—	—	instRingEquivClass ext
refl_apply 📖	mathematical	—	DFunLike.coe OrderRingIso EquivLike.toFunLike instEquivLike refl	—	—
self_trans_symm 📖	mathematical	—	trans symm refl	—	ext Equiv.left_inv
symm_apply_apply 📖	mathematical	—	DFunLike.coe OrderRingIso EquivLike.toFunLike instEquivLike symm	—	RingEquiv.symm_apply_apply
symm_apply_lt 📖	mathematical	—	Preorder.toLT DFunLike.coe OrderRingIso Preorder.toLE EquivLike.toFunLike instEquivLike symm	—	instOrderIsoClass toOrderIso_eq_coe OrderIso.symm_apply_lt
symm_bijective 📖	mathematical	—	Function.Bijective OrderRingIso symm	—	Function.bijective_iff_has_inverse symm_symm
symm_symm 📖	mathematical	—	symm	—	—
symm_trans_self 📖	mathematical	—	trans symm refl	—	ext Equiv.right_inv
toFun_eq_coe 📖	mathematical	—	Equiv.toFun RingEquiv.toEquiv toRingEquiv DFunLike.coe OrderRingIso EquivLike.toFunLike instEquivLike	—	—
toOrderIso_eq_coe 📖	mathematical	—	toOrderIso OrderIsoClass.toOrderIso OrderRingIso instEquivLike instOrderIsoClass	—	OrderIso.ext instOrderIsoClass
toOrderRingHom_eq_coe 📖	mathematical	—	toOrderRingHom OrderRingHomClass.toOrderRingHom OrderRingIso Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd Preorder.toLE EquivLike.toFunLike instEquivLike OrderIsoClass.toOrderHomClass instOrderIsoClass RingEquivClass.toRingHomClass instRingEquivClass	—	—
toOrderRingHom_injective 📖	mathematical	—	OrderRingIso Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd Preorder.toLE OrderRingHom toOrderRingHom	—	DFunLike.coe_injective DFunLike.ext'_iff
toRingEquiv_eq_coe 📖	mathematical	—	toRingEquiv RingEquivClass.toRingEquiv OrderRingIso instEquivLike instRingEquivClass	—	RingEquiv.ext instRingEquivClass
trans_apply 📖	mathematical	—	DFunLike.coe OrderRingIso EquivLike.toFunLike instEquivLike trans	—	—
trans_toRingEquiv 📖	mathematical	—	toRingEquiv trans RingEquiv.trans	—	—
trans_toRingEquiv_aux 📖	mathematical	—	RingEquivClass.toRingEquiv OrderRingIso instEquivLike instRingEquivClass trans RingEquiv.trans toRingEquiv	—	instRingEquivClass

OrderRingIso.Simps

Definitions

Name	Category	Theorems
symm_apply 📖	CompOp	—

OrderRingIsoClass

Definitions

Name	Category	Theorems
toOrderRingIso 📖	CompOp	—

(root)

Definitions

Name	Category	Theorems
OrderRingHom 📖	CompData	95 math math: OrderRingHom.coe_orderAddMonoidHom_apply, Cardinal.natCast_lt_toENat_iff, ArchimedeanClass.FiniteResidueField.mk_ratCast, Subring.orderedSubtype_coe, Set.toENat_cardinalMk_subtype, Cardinal.toENat_eq_natCast_iff, Cardinal.toENat_ofENat, Module.length_of_free, ArchimedeanClass.FiniteResidueField.ofArchimedean_apply, ArchimedeanClass.FiniteResidueField.mk_eq_zero, OrderRingIso.coe_toOrderRingHom, Submodule.spanRank_toENat_eq_iInf_encard, Cardinal.toENat_eq_zero, OrderRingHom.apply_eq_self, Cardinal.toENat_eq_ofNat, OrderRingHom.coe_coe_ringHom, OrderRingHom.coe_orderAddMonoidHom_id, Cardinal.toENat_lt_natCast_iff, Cardinal.toENat_lift, Cardinal.toENat_le_ofNat, ArchimedeanClass.stdPart_eq_sInf, ArchimedeanClass.mk_map_nonneg_of_archimedean, ArchimedeanClass.FiniteResidueField.ofArchimedean_inj, OrderRingHom.coe_comp, Ideal.height_le_spanRank_toENat_of_mem_minimal_primes, ArchimedeanClass.stdPart_map_real, ArchimedeanClass.lt_of_pos_of_archimedean, ArchimedeanClass.mk_sub_stdPart_pos, OrderRingHom.instOrderHomClass, ArchimedeanClass.FiniteResidueField.ofArchimedean_injective, LinearOrderedField.inducedOrderRingHom_toFun, OrderRingHom.ext_iff, OrderRingHom.coe_orderMonoidWithZeroHom_id, ArchimedeanClass.lt_of_lt_stdPart, OrderRingHom.coe_coe_orderMonoidWithZeroHom, OrderRingHom.toOrderMonoidWithZeroHom_eq_coe, OrderRingHom.toFun_eq_coe, OrderRingHom.coe_id, Cardinal.toNat_toENat, ArchimedeanClass.FiniteResidueField.mk_eq_mk, ArchimedeanClass.lt_of_stdPart_lt, OrderRingHom.toOrderAddMonoidHom_eq_coe, toENat_rank_span_set, OrderRingHom.instRingHomClass, Cardinal.toENat_strictMonoOn, OrderRingHom.coe_ringHom_id, Submodule.spanRank_toENat_eq_iInf_finset_card, OrderRingHom.coe_coe_orderAddMonoidHom, Cardinal.continuum_toENat, ArchimedeanClass.FiniteResidueField.mk_le_mk, OrderRingHom.coe_ringHom_apply, OrderRingHom.toRingHom_eq_coe, Cardinal.toENat_le_iff_of_le_aleph0, Cardinal.toENat_eq_top, OrderRingIso.toOrderRingHom_injective, ArchimedeanClass.ofArchimedean_stdPart, Cardinal.toENat_le_natCast_iff, Set.toENat_cardinalMk, Cardinal.enat_gc, ArchimedeanClass.lt_of_neg_of_archimedean, ArchimedeanClass.mk_le_mk_add_of_archimedean, Cardinal.toENat_le_nat, ArchimedeanClass.mk_sub_pos_iff, OrderRingHom.coe_orderMonoidWithZeroHom_apply, OrderRingHom.subsingleton, ArchimedeanClass.mk_le_add_mk_of_archimedean, ArchimedeanClass.FiniteResidueField.mk_lt_mk, Cardinal.toENat_comp_ofENat, Cardinal.toENat_le_iff_of_lt_aleph0, ArchimedeanClass.FiniteResidueField.ordConnected_preimage_mk, Cardinal.ofENat_toENat_le, Cardinal.toENat_le_one, Cardinal.toENat_injOn, LinearIndepOn.encard_le_toENat_rank, Cardinal.toENat_eq_nat, Cardinal.ofENat_toENat_eq_self, Cardinal.ofENat_toENat, OrderRingHom.id_apply, Cardinal.aleph_toENat, OrderRingHom.comp_apply, Cardinal.toENat_eq_iff_of_le_aleph0, ArchimedeanClass.stdPart_of_mk_nonneg, Ideal.height_le_spanRank_toENat, Cardinal.natCast_eq_toENat_iff, Cardinal.toENat_nat, Matroid.toENat_cRank_eq, ArchimedeanClass.mk_map_of_archimedean', Cardinal.natCast_le_toENat_iff, Module.length_eq_rank, Cardinal.toENat_lt_top, Cardinal.toENat_congr, Matroid.toENat_cRk_eq, Cardinal.toENat_eq_one, ArchimedeanClass.stdPart_eq_sSup, Hyperreal.coeRingHom_toFun
OrderRingIso 📖	CompData	31 math math: OrderRingIso.ext_iff, OrderRingIso.trans_toRingEquiv_aux, OrderRingIso.symm_bijective, OrderRingIso.apply_symm_apply, Valuation.IsEquiv.orderRingIso_apply, OrderRingIso.coe_toOrderRingHom, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, OrderRingIso.toRingEquiv_eq_coe, OrderRingIso.subsingleton_right, OrderRingIso.coe_ringEquiv_refl, OrderRingIso.trans_apply, OrderRingIso.subsingleton_left, OrderRingIso.coe_mk, OrderRingIso.symm_apply_apply, OrderRingIso.toOrderIso_eq_coe, OrderRingIso.lt_symm_apply, OrderRingIso.apply_eq_self, OrderRingIso.coe_toOrderRingHom_refl, OrderRingIso.toOrderRingHom_injective, LinearOrderedField.coe_inducedOrderRingIso, OrderRingIso.toOrderRingHom_eq_coe, OrderRingIso.refl_apply, OrderRingIso.instRingEquivClass, OrderRingIso.symm_apply_lt, OrderRingIso.instOrderIsoClass, OrderRingIso.coe_toOrderIso, OrderRingIso.coe_toRingEquiv, OrderRingIso.toFun_eq_coe, OrderRingIso.coe_orderIso_refl, Valuation.IsEquiv.orderRingIso_symm_apply
instCoeTCOrderRingHomOfOrderHomClassOfRingHomClass 📖	CompOp	—
instCoeTCOrderRingIsoOfOrderIsoClassOfRingEquivClass 📖	CompOp	—
«term_→+*o_» 📖	CompOp	—
«term_≃+*o_» 📖	CompOp	—

---

← Back to Index