Equiv

📁 Source: Mathlib/Algebra/Ring/Equiv.lean

Statistics

Metric	Count
Definitions toRingEquiv, toRingEquiv, inverse, symm_apply, cast, instEquivLike, instInhabited, instUnique, ofBijective, ofHomInv, ofHomInv', ofNonUnitalRingHom, ofRingHom, ofUnique, op, opOp, piCongrLeft, piCongrLeft', piCongrRight, piEquivPiSubtypeProd, piMulOpposite, piOptionEquivProd, piUnique, prodCongr, refl, sumArrowEquivProdArrow, aux, toAddEquiv, toAddMonoidHom, toEquiv, toMonoidHom, toMulEquiv, toNonUnitalRingHom, toOpposite, toRingHom, trans, unop, RingEquivClass, toRingEquiv, inverse, instCoeTCRingEquivOfRingEquivClass, «term_≃+*_»	42
Theorems isCancelMulZero_iff, isDomain, isDomain_iff, isLeftCancelMulZero_iff, isRightCancelMulZero_iff, noZeroDivisors, noZeroDivisors_iff, inverse_apply, apply_symm_apply, bijective, cast_apply, cast_symm_apply, coe_addEquiv_refl, coe_addEquiv_trans, coe_addMonoidHom_refl, coe_addMonoidHom_trans, coe_mk, coe_monoidHom_refl, coe_monoidHom_trans, coe_mulEquiv_refl, coe_mulEquiv_trans, coe_nonUnitalRingHom_inj_iff, coe_ofBijective, coe_prodCongr, coe_refl, coe_ringHom_inj_iff, coe_ringHom_ofRingHom, coe_ringHom_refl, coe_ringHom_trans, coe_toAddEquiv, coe_toAddEquiv_symm, coe_toEquiv, coe_toEquiv_symm, coe_toMulEquiv, coe_toMulEquiv_symm, coe_toNonUnitalRingHom, coe_toRingHom, coe_trans, comp_ofBijective_symm, comp_symm, congr_arg, congr_fun, eq_symm_apply, ext, ext_iff, image_eq_preimage, image_eq_preimage_symm, image_symm_eq_preimage, injective, instRingEquivClass, invFun_eq_symm, map_add, map_add', map_eq_neg_one_iff, map_eq_one_iff, map_eq_zero_iff, map_mul, map_mul', map_ne_one_iff, map_ne_zero_iff, map_neg, map_neg_one, map_one, map_pow, map_sub, map_zero, mk_coe, mk_coe', ofBijective_apply, ofBijective_symm_comp, ofHomInv'_apply, ofHomInv'_symm_apply, ofHomInv_apply, ofHomInv_symm_apply, ofNonUnitalRingHom_apply, ofNonUnitalRingHom_symm_apply, ofRingHom_apply, ofRingHom_coe_ringHom, ofRingHom_symm, ofRingHom_symm_apply, opOp_apply, opOp_symm_apply, op_apply_apply, op_apply_symm_apply, op_symm_apply_apply, op_symm_apply_symm_apply, piCongrLeft'_apply, piCongrLeft'_symm, piCongrLeft'_symm_apply, piCongrLeft_apply, piCongrLeft_symm_apply, piCongrRight_apply, piCongrRight_refl, piCongrRight_symm, piCongrRight_trans, piEquivPiSubtypeProd_apply, piEquivPiSubtypeProd_symm_apply, piOptionEquivProd_apply, piOptionEquivProd_symm_apply, piUnique_apply, piUnique_symm_apply, prodCongr_apply, prodCongr_symm_apply, refl_apply, self_trans_symm, sumArrowEquivProdArrow_apply, sumArrowEquivProdArrow_symm_apply, surjective, symm_apply_apply, symm_apply_eq, symm_bijective, symm_comp, symm_mk, symm_ofNonUnitalRingHom, symm_refl, symm_symm, symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply, symm_toNonUnitalRingHom_comp_toNonUnitalRingHom, symm_toRingHom_apply_toRingHom_apply, symm_toRingHom_comp_toRingHom, symm_trans, symm_trans_apply, symm_trans_self, toAddEquiv_eq_coe, toAddMonoidHom_refl, toAddMonoidMom_commutes, toEquiv_commutes, toEquiv_eq_coe, toMonoidHom_commutes, toMonoidHom_refl, toMulEquiv_eq_coe, toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply, toNonUnitalRingHom_commutes, toNonUnitalRingHom_eq_coe, toNonUnitalRingHom_injective, toNonUnitalRingHom_refl, toNonUnitalRingHom_trans, toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom, toOpposite_apply, toOpposite_symm_apply, toRingHom_apply_symm_toRingHom_apply, toRingHom_comp_symm_toRingHom, toRingHom_eq_coe, toRingHom_injective, toRingHom_refl, toRingHom_trans, trans_apply, map_add, toAddEquivClass, toMulEquivClass, toNonUnitalRingHomClass, toRingHomClass, inverse_apply	153
Total	195

AddEquiv

Definitions

Name	Category	Theorems
toRingEquiv 📖	CompOp	—

MulEquiv

Definitions

Name	Category	Theorems
toRingEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCancelMulZero_iff 📖	mathematical	—	IsCancelMulZero MulZeroClass.toMul MulZeroClass.toZero	—	Function.Injective.isCancelMulZero injective map_zero MulEquivClass.toZeroHomClass instMulEquivClass map_mul MulEquivClass.instMulHomClass
isDomain 📖	mathematical	—	IsDomain	—	Function.Injective.isLeftCancelMulZero injective map_zero MonoidWithZeroHomClass.toZeroHomClass MulEquivClass.toMonoidWithZeroHomClass instMulEquivClass map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero Function.Injective.isRightCancelMulZero IsCancelMulZero.toIsRightCancelMulZero zero_ne_one NeZero.one IsDomain.toNontrivial
isDomain_iff 📖	mathematical	—	IsDomain	—	isDomain
isLeftCancelMulZero_iff 📖	mathematical	—	IsLeftCancelMulZero MulZeroClass.toMul MulZeroClass.toZero	—	Function.Injective.isLeftCancelMulZero injective map_zero MulEquivClass.toZeroHomClass instMulEquivClass map_mul MulEquivClass.instMulHomClass
isRightCancelMulZero_iff 📖	mathematical	—	IsRightCancelMulZero MulZeroClass.toMul MulZeroClass.toZero	—	Function.Injective.isRightCancelMulZero injective map_zero MulEquivClass.toZeroHomClass instMulEquivClass map_mul MulEquivClass.instMulHomClass
noZeroDivisors 📖	mathematical	—	NoZeroDivisors MulZeroClass.toMul MulZeroClass.toZero	—	Function.Injective.noZeroDivisors injective map_zero MulEquivClass.toZeroHomClass instMulEquivClass map_mul MulEquivClass.instMulHomClass
noZeroDivisors_iff 📖	mathematical	—	NoZeroDivisors MulZeroClass.toMul MulZeroClass.toZero	—	noZeroDivisors

NonUnitalRingHom

Definitions

Name	Category	Theorems
inverse 📖	CompOp	1 math math: inverse_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverse_apply 📖	mathematical	DFunLike.coe NonUnitalRingHom instFunLike	inverse	—	—

RingEquiv

Definitions

Name	Category	Theorems
cast 📖	CompOp	2 math math: cast_apply, cast_symm_apply
instEquivLike 📖	CompOp	617 math math: MonoidAlgebra.mapDomainRingEquiv_single, AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs, piCongrRight_apply, RCLike.sqrt_eq_ite, AddMonoidAlgebra.mapDomainRingEquiv_apply, apply_symm_apply, toRingCatIso_inv, coe_ringHom_trans, Language.reverseIso_apply, Polynomial.roots_expand, toOpposite_symm_apply, FractionalIdeal.mapEquiv_apply, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, Int.quotientSpanEquivZMod_comp_Quotient_mk, frobeniusEquiv_apply, BitVec.equivFin_symm_apply_toFin, coe_addEquiv_refl, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_apply_mk, WithAbs.algebraMap_left_apply, iterateFrobeniusEquiv_symm_add_apply, coe_frobeniusEquiv_symm_comp_coe_frobenius, coe_prodComm_symm, surjective, ofHomInv'_apply, RingHom.IsStandardSmoothOfRelativeDimension.equiv, op_apply_apply, idealComapOrderIso_apply, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, IsPerfectClosure.equiv_comp_equiv_apply_eq_self, asBoolRingAsBoolAlg_apply, MvPolynomial.isEmptyRingEquiv_apply, Polynomial.opRingEquiv_op_monomial, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm, FDRep.endRingEquiv_symm_comp_ρ, toOpposite_apply, map_sub, BoolRing.Iso.mk_hom_hom', LaurentSeries.LaurentSeriesRingEquiv_def, toEquiv_commutes, LocallyConstant.congrLeftRingEquiv_apply_apply, RingHomSurjective.instToRingHomRingEquiv, RingHom.quotientKerEquivOfSurjective_symm_apply, WittVector.IsocrystalHom.frob_equivariant, NumberField.CMExtension.algebraMap_equivMaximalRealSubfield_symm_apply, AlgEquiv.toRingEquiv_toRingHom, WittVector.frobeniusEquiv_symm_apply, prodProdProdComm_apply, Ideal.comap_symm, AlgEquiv.coe_ringEquiv', map_list_sum, Int.quotientSpanNatEquivZMod_comp_Quotient_mk, map_neg, RingAut.smul_def, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, NonUnitalSubsemiring.coe_equivMapOfInjective_apply, AddMonoidAlgebra.toRingHom_mapRangeRingEquiv, NonUnitalSubsemiring.mem_map_equiv, MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply, PowerBasis.quotientEquivQuotientMinpolyMap_apply, NonUnitalSubring.map_equiv_eq_comap_symm, Submodule.LinearDisjoint.op, RestrictScalars.ringEquiv_algebraMap, MonoidAlgebra.opRingEquiv_single, Valuation.IsEquiv.orderRingIso_apply, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, rootsOfUnity.integer_power_of_ringEquiv, Polynomial.leadingCoeff_opRingEquiv, toCommSemiRingCatIso_inv, Subring.centerCongr_apply_coe, mopMatrix_symm_apply, NonUnitalSubsemiring.centerCongr_symm_apply_coe, ofLeftInverse_symm_apply, NumberField.InfinitePlace.Completion.norm_coe, iterateFrobeniusEquiv_def, piOptionEquivProd_apply, op_apply_symm_apply, RingCon.comapQuotientEquivRange_symm_mk, piCongrLeft_symm_apply, ofLeftInverse_apply, snd_comp_coe_prodComm, RCLike.realRingEquiv_symm_apply, BoolRing.Iso.mk_inv_hom', RingCon.comapQuotientEquivOfSurj_symm_mk, ext_iff, piCongrLeft'_apply, NonUnitalSubring.centerCongr_apply_coe, ofHomInv_symm_apply, mopMatrix_apply, Subsemiring.centerCongr_symm_apply_coe, MonoidAlgebra.opRingEquiv_symm_apply, NumberField.RingOfIntegers.withValEquiv_symm_apply, WithAbs.equiv_algebraMap_apply, Matrix.uniqueRingEquiv_apply, coe_toMulEquiv, ModuleCat.endRingEquiv_symm_apply_hom, map_mul, frobeniusEquiv_symm_comp_frobenius, AddMonoidAlgebra.uniqueRingEquiv_apply, IsLocalization.isLocalization_iff_of_base_ringEquiv, MvPolynomial.mvPolynomialEquivMvPolynomial_apply, MonoidHom.map_frobeniusEquiv_symm, MonoidAlgebra.uniqueRingEquiv_apply, AddMonoidAlgebra.opRingEquiv_symm_single, modularCyclotomicCharacter.spec, ofLeftInverseS_symm_apply, AddMonoidAlgebra.opRingEquiv_symm_apply, MulSemiringAction.toRingEquiv_apply, NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe, modularCyclotomicCharacter.toFun_spec', quotientBot_symm_mk, Ideal.quotEquivOfEq_mk, Ideal.comap_of_equiv, Polynomial.mapEquiv_symm_apply, MonoidAlgebra.mapRangeRingEquiv_single, Subring.mopRingEquivOp_apply_coe, BialgEquiv.toRingEquiv_toRingHom, RCLike.complexRingEquiv_apply, Rat.IsIntegralClosure.intEquiv_apply_eq_ringOfIntegersEquiv, DoubleQuot.quotQuotEquivComm_comp_quotQuotMk, asBoolRingAsBoolAlg_symm_apply, DoubleQuot.quotQuotEquivComm_quotQuotMk, HahnSeries.toMvPowerSeries_symm_apply_coeff, toNonUnitalRingHom_commutes, PreTilt.coeff_frobeniusEquiv_symm, RingCon.comapQuotientEquivRangeS_symm_mk, moduleEndSelf_symm_apply, Matrix.transposeRingEquiv_symm_apply, Subsemiring.coe_equivMapOfInjective_apply, starRingAut_apply, Matrix.piRingEquiv_apply, NonUnitalSubring.topEquiv_symm_apply_coe, instRingEquivClass, Polynomial.opRingEquiv_op_C, coe_ofBijective, Polynomial.roots_X_pow_char_pow_sub_C_pow, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, iterateFrobeniusEquiv_add_apply, WithVal.apply_symm_equiv, IsLocalization.ringEquivOfRingEquiv_symm_apply, symm_apply_apply, sofLeftInverse'_apply, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, RingAut.one_apply, map_neg_one, cast_apply, gelfandStarTransform_symm_apply, Matrix.piRingEquiv_symm_apply, WithAbs.tendsto_one_div_one_add_pow_nhds_one, RingCon.comapQuotientEquivRange_mk, symm_apply_eq, AlgEquiv.op_apply_symm_apply, WithVal.apply_equiv, piEquivPiSubtypeProd_symm_apply, quotientBot_mk, prodZeroRing_symm_apply, ofBijective_apply, Subring.comap_equiv_eq_map_symm, zeroRingProd_symm_apply, Valuation.IsEquiv.uniformContinuous_equivWithVal, map_one, injective, map_eq_zero_iff, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, map_zero, MvPolynomial.mapEquiv_apply, WithAbs.algebraMap_right_apply, WittVector.IsocrystalEquiv.frob_equivariant, Subsemiring.centerCongr_apply_coe, map_eq_one_iff, modularCyclotomicCharacter.toFun_spec, coe_ringEquiv_lpBCF, NonUnitalSubring.topEquiv_apply, toCommRingCatIso_inv, toAddMonoidMom_commutes, FractionalIdeal.canonicalEquiv_mk0, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, moduleEndSelfOp_apply, AdjoinRoot.quotEquivQuotMap_apply, congr_arg, Subring.centerToMulOpposite_symm_apply_coe, toRingCatIso_hom, Subsemiring.mem_map_equiv, coe_toAddEquiv, ZMod.ringEquivCongr_refl_apply, Subring.topEquiv_apply, subsemiringMap_apply_coe, coe_mk, IsFractionRing.ringEquivOfRingEquiv_algebraMap, MvPolynomial.isEmptyRingEquiv_symm_apply, Subring.mopRingEquivOp_symm_apply, NonUnitalSubsemiring.map_equiv_eq_comap_symm, Polynomial.opRingEquiv_op_X, Subsemiring.centerToMulOpposite_symm_apply_coe, TruncatedWittVector.commutes_symm', invFun_eq_symm, piEquivPiSubtypeProd_apply, map_add, toCommRingCatIso_hom, CategoryTheory.Iso.ringCatIsoToRingEquiv_toRingHom, MonoidAlgebra.opRingEquiv_symm_single, IsLocalization.ringEquivOfRingEquiv_eq_map, PreTilt.coeff_iterate_frobeniusEquiv_symm, IsLocalRing.ResidueField.mapEquiv_apply, DoubleQuot.coe_quotQuotEquivQuotSupₐ, Ideal.quotientMulEquivQuotientProd_snd, AddMonoidAlgebra.commRingEquiv_single_single, Module.End.ringEquivEndFinsupp_apply_apply_apply, map_list_prod, Subring.mem_map_equiv, FractionalIdeal.canonicalEquiv_spanSingleton, Ideal.symm_apply_mem_of_equiv_iff, Matrix.compRingEquiv_symm_apply, NumberField.CMExtension.equivMaximalRealSubfield_apply, moduleEndSelf_apply, Ideal.fst_comp_quotientMulEquivQuotientProd, ofHomInv_apply, ZMod.ringEquivCongr_ringEquivCongr_apply, NonUnitalSubring.centerCongr_symm_apply_coe, Subsemiring.centerToMulOpposite_apply_coe, IsAlgClosure.equivOfEquiv_comp_algebraMap, coe_addMonoidHom_refl, Submodule.equivOpposite_apply, RingCon.quotientQuotientEquivQuotient_coe_coe, MonoidAlgebra.curryRingEquiv_symm_single, ofRingHom_symm_apply, WithVal.lt_def, coe_mulEquiv_trans, AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero, Int.quotientSpanEquivZMod_comp_castRingHom, RingCon.quotientKerEquivOfRightInverse_apply, Matrix.transposeRingEquiv_apply, prodCongr_apply, OrderRingIso.coe_mk, LocallyConstant.congrLeftRingEquiv_symm_apply_apply, frobeniusEquiv_symm_pow, evalRingHom_mapMatrix_comp_compRingEquiv, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, map_det, LinearEquiv.conjRingEquiv_apply_apply, subsemiringMap_symm_apply_coe, RingCon.comapQuotientEquivRangeS_mk, trans_apply, coe_frobeniusEquiv, coe_ringHom_inj_iff, addMonoidEndRingEquivInt_apply, quotAdjoinEquivQuotMap_apply_mk, mapTwoSidedIdeal_apply, MulSemiringAction.toAlgEquiv_toEquiv, WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, LaurentSeries.coe_X_compare, FractionalIdeal.canonicalEquiv_coeIdeal, toNonUnitalRingHom_eq_coe, frobenius_comp_frobeniusEquiv_symm, PerfectionMap.comp_equiv', ofNonUnitalRingHom_apply, Subring.topEquiv_symm_apply_coe, RingCon.coe_comapQuotientEquivRange_mk, IsAlgClosure.equivOfEquiv_symm_algebraMap, AlgEquiv.coe_ringEquiv, RingCon.coe_quotientKerEquivRangeS_mk, iterateFrobeniusEquiv_one_apply, coe_nonUnitalRingHom_inj_iff, idealComapOrderIso_symm_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, IsPerfectClosure.equiv_comp, Rat.HeightOneSpectrum.natGenerator_dvd_iff, comp_ofBijective_symm, Polynomial.roots_X_pow_char_sub_C_pow, WittVector.inv_pair₂, Subring.centerToMulOpposite_apply_coe, WittVector.exists_frobenius_solution_fractionRing, MulSemiringAction.toRingEquiv_symm_apply, LaurentSeries.exists_powerSeries_of_memIntegers, Ideal.quotEquivOfEq_eq_factor, coe_frobenius_comp_coe_frobeniusEquiv_symm, AlgEquiv.op_symm_apply_symm_apply, FractionalIdeal.coeFun_mapEquiv, coe_toEquiv, sumArrowEquivProdArrow_symm_apply, Ring.DirectLimit.ringEquiv_of, RingHom.quotientKerEquivOfRightInverse.Symm.apply, IsLocalization.AtPrime.equivQuotMaximalIdeal_apply_mk, height_comap, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, RingCon.congr_mk, FractionalIdeal.canonicalEquiv_canonicalEquiv, map_prod, WittVector.inv_pair₁, WithAbs.norm_eq_abv, Matrix.conjTransposeRingEquiv_symm_apply, MonoidAlgebra.mapRangeRingEquiv_apply, cast_symm_apply, map_pow, prodZeroRing_apply, RingHom.quotientKerEquivOfSurjective_apply_mk, Subsemiring.mopRingEquivOp_apply_coe, IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply, IsPerfectClosure.equiv_self_apply, toEquiv_eq_coe, PerfectionMap.comp_equiv, piUnique_symm_apply, Ideal.pointwise_smul_eq_comap, mapMatrix_apply, Ideal.snd_comp_quotientMulEquivQuotientProd, HahnSeries.coeff_toPowerSeries, RingHom.map_iterate_frobeniusEquiv_symm, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, RestrictScalars.ringEquiv_map_smul, frobeniusEquiv_def, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, Ideal.quotientInfEquivQuotientProd_snd, Polynomial.opRingEquiv_symm_C_mul_X_pow, coe_prodComm, toMonoidHom_commutes, Polynomial.opRingEquiv_symm_monomial, toCommSemiRingCatIso_hom, RingCon.quotientQuotientEquivQuotient_mk_mk, IsLocalization.algEquivOfAlgEquiv_symm_apply, Submodule.linearDisjoint_op, NonUnitalSubring.comap_equiv_eq_map_symm, IsPerfectClosure.equiv_comp_equiv_apply, Rat.HeightOneSpectrum.span_natGenerator, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ, PerfectRing.lift_apply, Ideal.apply_mem_of_equiv_iff, Polynomial.support_opRingEquiv, PerfectionMap.comp_symm_equiv, RingHom.rangeRestrictFieldEquiv_apply_symm_apply, RCLike.complexRingEquiv_symm_apply, ofLeftInverse'_symm_apply, WithAbs.equivWithAbs_equiv_symm_apply, prodProdProdComm_toMulEquiv, FractionalIdeal.canonicalEquiv_flip, IsLocalization.isLocalization_of_base_ringEquiv, AddMonoidAlgebra.opRingEquiv_single, Subring.map_equiv_eq_comap_symm, NonUnitalSubsemiring.comap_equiv_eq_map_symm, HahnSeries.coeff_toPowerSeries_symm, AlgEquiv.opComm_apply_symm_apply, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, WithAbs.equiv_equivWithAbs_symm_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, IsPerfectClosure.equiv_apply, Matrix.uniqueRingEquiv_symm_apply, IsAlgClosure.equivOfEquiv_symm_comp_algebraMap, height_map, NumberField.InfinitePlace.isReal_comap_iff, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, LaurentSeries.powerSeriesEquivSubring_apply, piCongrLeft_apply, iterate_frobeniusEquiv_symm_pow_p_pow, toSemilinearEquiv_symm_apply, NonUnitalSubring.centerToMulOpposite_symm_apply_coe, Ideal.map_of_equiv, RingAut.inv_apply, op_symm_apply_symm_apply, nonUnitalSubsemiringMap_symm_apply_coe, AddMonoidAlgebra.curryRingEquiv_symm_single, image_eq_preimage, AddMonoidAlgebra.opRingEquiv_apply, NonUnitalSubring.coe_equivMapOfInjective_apply, ofLeftInverse'_apply, AddMonoidAlgebra.mapDomainRingEquiv_single, MonoidAlgebra.curryRingEquiv_single, WittVector.StandardOneDimIsocrystal.frobenius_apply, Subring.centerCongr_symm_apply_coe, polynomial_expand_eq, coe_toEquiv_symm, iterateFrobeniusEquiv_apply, NonUnitalSubring.mem_map_equiv, Ideal.quotientMulEquivQuotientProd_fst, toAddEquiv_eq_coe, IsAlgClosure.equivOfEquiv_algebraMap, Rat.ringOfIntegersEquiv_apply_coe, Subring.ringEquivOpMop_symm_apply_coe, LocallyConstant.congrRightRingEquiv_apply_apply, HahnSeries.coeff_toMvPowerSeries_symm, MonoidAlgebra.uniqueRingEquiv_symm_apply, RingInvo.coe_ringEquiv, Ideal.map_comap_of_equiv, symm_trans_apply, congr_fun, Polynomial.coeff_opRingEquiv, Ideal.map_symm, IsPerfectClosure.equiv_comp_apply, WittVector.quotientPEquiv_mk, NumberField.RingOfIntegers.mapRingEquiv_apply, LocallyConstant.congrRightRingEquiv_symm_apply_apply, Polynomial.toFinsuppIso_apply, AddMonoidAlgebra.uniqueRingEquiv_symm_apply, Subsemiring.ringEquivOpMop_symm_apply_coe, ofNonUnitalRingHom_symm_apply, LaurentSeries.powerSeriesEquivSubring_coe_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, DoubleQuot.quotQuotEquivQuotSup_quotQuotMk, toSemiRingCatIso_hom, Ring.DirectLimit.ringEquiv_symm_mk, coe_ringHom_refl, frobeniusEquiv_symm_pow_p, Padic.withValUniformEquiv_cast_apply, RingAut.coe_one, map_sum, Padic.coe_withValRingEquiv, frobenius_apply_frobeniusEquiv_symm, TruncatedWittVector.zmodEquivTrunc_apply, ofRingHom_apply, trace_quotient_eq_trace_localization_quotient, Perfection.coeff_frobeniusEquiv_symm, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, coe_prodCongr, AddMonoidAlgebra.mapRangeRingEquiv_apply, toMulEquiv_eq_coe, LinearEquiv.conjRingEquiv_symm_apply_apply, piCongrLeft'_symm_apply, toSemilinearEquiv_apply, Perfection.lift_apply_apply_coe, zeroRingProd_apply, RingHom.ker_coe_equiv, RingHomInvPair.of_ringEquiv, PreTilt.untilt_iterate_frobeniusEquiv_symm_pow, op_symm_apply_apply, MonoidAlgebra.toRingHom_mapRangeRingEquiv, NonUnitalSubsemiring.centerToMulOpposite_apply_coe, HahnSeries.coeff_toMvPowerSeries, RCLike.realRingEquiv_apply, MonoidAlgebra.mapDomainRingEquiv_apply, PerfectionMap.surjective, AlgebraicGeometry.Proj.stalkIso'_germ, cyclotomicCharacter.spec, Subsemiring.topEquiv_symm_apply_coe, sumArrowEquivProdArrow_apply, image_eq_preimage_symm, WithVal.equivWithVal_apply, AlgEquiv.opComm_symm_apply_symm_apply, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, Padic.coe_withValRingEquiv_symm, sofLeftInverse'_symm_apply, Polynomial.roots_X_pow_char_sub_C, Ideal.quotientInfEquivQuotientProd_fst, WittVector.quotEquivOfEq_ghostComponentModPPow, AdjoinRoot.quotEquivQuotMap_symm_apply, WittVector.exists_frobenius_solution_fractionRing_aux, IsPerfectClosure.equiv_symm_apply, toRingHom_eq_coe, map_multiset_sum, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, IsLocalization.ringEquivOfRingEquiv_eq, FractionalIdeal.map_canonicalEquiv_mk0, Rat.ringOfIntegersEquiv_symm_apply_coe, coe_ringHom_ofRingHom, Polynomial.opRingEquiv_symm_C, FractionalIdeal.mem_canonicalEquiv_apply, rootsOfUnity.integer_power_of_ringEquiv', piFinTwo_symm_apply, WittVector.frobeniusEquiv_apply, symm_comp, HahnSeries.ofPowerSeries_apply, RingHom.quotientKerEquivOfRightInverse.apply, Subsemiring.ringEquivOpMop_apply, CategoryTheory.Iso.commRingCatIsoToRingEquiv_toRingHom, Polynomial.roots_expand_pow, HahnSeries.toMvPowerSeries_apply, modularCyclotomicCharacter'.spec', Module.End.ringEquivEndFinsupp_apply_apply_support, Subsemiring.map_equiv_eq_comap_symm, CategoryTheory.Iso.semiRingCatIsoToRingEquiv_toRingHom, coe_ringEquiv_lpBCF_symm, Polynomial.toFinsuppIso_symm_apply, map_eq_neg_one_iff, unop_map_list_prod, map_multiset_prod, coe_addEquiv_trans, PerfectionMap.comp_symm_equiv', IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_apply_mk, DoubleQuot.quotQuotEquivComm_mk_mk, Matrix.conjTransposeRingEquiv_apply, Matrix.compRingEquiv_apply, coe_addMonoidHom_trans, Language.reverseIso_symm_apply, ofLeftInverseS_apply, NumberField.InfinitePlace.Completion.WithAbs.ratCast_equiv, Submodule.equivOpposite_symm_apply, Polynomial.natDegree_opRingEquiv, LaurentSeries.ratfuncAdicComplRingEquiv_apply, AddMonoidAlgebra.curryRingEquiv_single, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk, coe_toAddEquiv_symm, Equiv.ringEquiv_apply, Perfection.coeff_iterate_frobeniusEquiv_symm, Subsemiring.comap_equiv_eq_map_symm, DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk, coe_trans, starRingEquiv_apply, WithVal.le_def, NumberField.ComplexEmbedding.isReal_comp_iff, addMonoidAlgebraRingEquivDirectSum_apply, RingAut.mul_apply, Submodule.mulMap_op, eq_symm_apply, addMonoidEndRingEquivInt_symm_apply, DoubleQuot.coe_quotQuotEquivCommₐ, addMonoidAlgebraRingEquivDirectSum_symm_apply, image_symm_eq_preimage, coe_toMulEquiv_symm, Ideal.fst_comp_quotientInfEquivQuotientProd, coe_monoidHom_trans, Ideal.map_prodComm_prod, NonUnitalSubsemiring.centerCongr_apply_coe, Real.ringEquivCauchy_apply, Polynomial.opRingEquiv_op_C_mul_X_pow, Subring.coe_equivMapOfInjective_apply, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, TruncatedWittVector.commutes', RingCon.quotientQuotientEquivQuotient_symm_mk, DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap, IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk, IsLocalization.ringEquivOfRingEquiv_apply, DoubleQuot.quotQuotEquivQuotOfLE_symm_mk, opOp_symm_apply, ClassGroup.mk_canonicalEquiv, ValuationRing.coe_equivInteger_apply, WithVal.valuation_equiv_symm, Subsemiring.mopRingEquivOp_symm_apply, RingHom.rangeRestrictFieldEquiv_apply_coe, bijective, ModuleCat.endRingEquiv_apply, WittVector.ghostEquiv_coe, RatFunc.toFractionRingRingEquiv_apply, coe_toNonUnitalRingHom, NumberField.InfiniteAdeleRing.ringEquiv_mixedSpace_apply, Module.compHom.toLinearEquiv_symm_apply, AlgEquiv.subalgebraMap_symm_apply_coe, Subsemiring.topEquiv_apply, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, ZMod.ringEquivCongr_val, LaurentSeries.mem_integers_of_powerSeries, Polynomial.mapEquiv_apply, PerfectRing.liftAux_apply, coe_iterateFrobeniusEquiv, HahnSeries.toPowerSeries_apply, Ideal.snd_comp_quotientInfEquivQuotientProd, coe_monoidHom_refl, MonoidHom.map_iterate_frobeniusEquiv_symm, ZMod.ringEquivCongr_intCast, ofHomInv'_symm_apply, RingCon.quotientKerEquivOfSurjective_mk, refl_apply, nonUnitalSubsemiringMap_apply_coe, Module.End.ringEquivEndFinsupp_symm_apply_apply, piOptionEquivProd_symm_apply, BitVec.equivFin_apply, Ideal.Factors.piQuotientEquiv_mk, Equiv.ringEquiv_symm_apply, piFinTwo_apply, PerfectionMap.lift_apply, NonUnitalSubring.centerToMulOpposite_apply_coe, prodProdProdComm_toEquiv, Subring.ringEquivOpMop_apply, HahnSeries.toPowerSeries_symm_apply_coeff, coe_toRingHom, AlgebraicGeometry.Proj.stalkIso'_symm_mk, piUnique_apply, fst_comp_coe_prodComm, WithVal.equivWithVal_symm_apply, StarRingEquiv.coe_mk, MonoidAlgebra.opRingEquiv_apply, opOp_apply, ofBijective_symm_comp, AbsoluteValue.isEquiv_iff_isHomeomorph, prodProdProdComm_toAddEquiv, NumberField.RingOfIntegers.mapRingEquiv_symm_apply, IsDedekindDomain.quotientEquivPiFactors_mk, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, MonoidAlgebra.commRingEquiv_single_single, Real.ringEquivCauchy_symm_apply_cauchy, ClassGroup.mk_def, modularCyclotomicCharacter.aux_spec, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, PerfectionMap.equiv_apply, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk, map_prime_of_equiv, Int.quotientSpanNatEquivZMod_comp_castRingHom, AddMonoidAlgebra.mapRangeRingEquiv_single, Polynomial.opRingEquiv_symm_X, RingHom.map_frobeniusEquiv_symm, modularCyclotomicCharacter.toFun_spec'', FDRep.endRingEquiv_comp_ρ, WithAbs.equivWithAbs_symm_equiv_symm_apply, cyclotomicCharacter.toFun_spec, Rat.ringOfIntegersWithValEquiv_apply, iterateFrobeniusEquiv_zero_apply, ClassGroup.equiv_mk, toSemiRingCatIso_inv, RingAut.coe_pow, DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk, OrderRingIso.coe_toRingEquiv, frobeniusEquiv_symm_apply_frobenius, coe_mulEquiv_refl, Polynomial.roots_X_pow_char_pow_sub_C, prodCongr_symm_apply, CategoryTheory.Iso.commSemiRingCatIsoToRingEquiv_toRingHom, Ideal.Factors.piQuotientEquiv_map, coe_refl, NonUnitalSubsemiring.topEquiv_symm_apply_coe, moduleEndSelfOp_symm_apply, Valuation.IsEquiv.orderRingIso_symm_apply, comp_symm, NonUnitalSubsemiring.topEquiv_apply, DoubleQuot.quotQuotEquivComm_algebraMap, IsLocalization.ringEquivOfRingEquiv_mk', AlgEquiv.coe_ringHom_commutes, RingCon.comapQuotientEquivOfSurj_mk, Module.compHom.toLinearEquiv_apply, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply
instInhabited 📖	CompOp	—
instUnique 📖	CompOp	—
ofBijective 📖	CompOp	6 math math: AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, coe_ofBijective, gelfandStarTransform_symm_apply, ofBijective_apply, comp_ofBijective_symm, ofBijective_symm_comp
ofHomInv 📖	CompOp	—
ofHomInv' 📖	CompOp	—
ofNonUnitalRingHom 📖	CompOp	5 math math: ofHomInv'_apply, ofNonUnitalRingHom_apply, symm_ofNonUnitalRingHom, ofNonUnitalRingHom_symm_apply, ofHomInv'_symm_apply
ofRingHom 📖	CompOp	7 math math: ofRingHom_coe_ringHom, ofHomInv_symm_apply, ofHomInv_apply, ofRingHom_symm_apply, ofRingHom_symm, ofRingHom_apply, coe_ringHom_ofRingHom
ofUnique 📖	CompOp	—
op 📖	CompOp	5 math math: op_apply_apply, op_apply_symm_apply, op_symm_apply_symm_apply, AlgEquiv.toRingEquiv_op, op_symm_apply_apply
opOp 📖	CompOp	3 math math: AlgEquiv.toRingEquiv_opOp, opOp_symm_apply, opOp_apply
piCongrLeft 📖	CompOp	2 math math: piCongrLeft_symm_apply, piCongrLeft_apply
piCongrLeft' 📖	CompOp	5 math math: piCongrLeft_symm_apply, piCongrLeft'_symm, piCongrLeft'_apply, piCongrLeft_apply, piCongrLeft'_symm_apply
piCongrRight 📖	CompOp	4 math math: piCongrRight_apply, piCongrRight_refl, piCongrRight_symm, piCongrRight_trans
piEquivPiSubtypeProd 📖	CompOp	2 math math: piEquivPiSubtypeProd_symm_apply, piEquivPiSubtypeProd_apply
piMulOpposite 📖	CompOp	—
piOptionEquivProd 📖	CompOp	2 math math: piOptionEquivProd_apply, piOptionEquivProd_symm_apply
piUnique 📖	CompOp	2 math math: piUnique_symm_apply, piUnique_apply
prodCongr 📖	CompOp	3 math math: prodCongr_apply, coe_prodCongr, prodCongr_symm_apply
refl 📖	CompOp	32 math math: RingAut.one_eq_refl, modularCyclotomicCharacter.id, coe_addEquiv_refl, IsLocalization.algEquiv_apply, Localization.algEquiv_apply, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, toAddMonoidHom_refl, OrderRingIso.coe_ringEquiv_refl, iterateFrobeniusEquiv_zero, piCongrRight_refl, IsLocalRing.ResidueField.mapEquiv_refl, coe_addMonoidHom_refl, IsPerfectClosure.equiv_self, symm_trans_self, toNonUnitalRingHom_refl, IsPerfectClosure.equiv_comp_equiv_eq_id, ZMod.ringEquivCongr_refl, toRingHom_refl, coe_ringHom_refl, toMonoidHom_refl, IsLocalization.algEquiv_symm_apply, FractionalIdeal.mapEquiv_refl, MvPolynomial.mapEquiv_refl, mapMatrix_refl, FractionalIdeal.canonicalEquiv_self, coe_monoidHom_refl, refl_apply, symm_refl, self_trans_symm, coe_mulEquiv_refl, coe_refl, Localization.algEquiv_symm_apply
sumArrowEquivProdArrow 📖	CompOp	2 math math: sumArrowEquivProdArrow_symm_apply, sumArrowEquivProdArrow_apply
toAddEquiv 📖	CompOp	3 math math: AlgEquiv.subalgebraMap_apply_coe, toAddEquiv_eq_coe, nonUnitalSubsemiringMap_apply_coe
toAddMonoidHom 📖	CompOp	1 math math: toAddMonoidHom_refl
toEquiv 📖	CompOp	14 math math: StarAlgEquiv.restrictScalars_symm_apply, map_add', RingInvo.involution', map_mul', RCLike.realLinearIsometryEquiv_symm_apply, RCLike.complexLinearIsometryEquiv_symm_apply, toEquiv_eq_coe, StarRingEquiv.map_star', OrderRingIso.map_le_map_iff', toSemilinearEquiv_symm_apply, StarAlgEquiv.map_smul', RCLike.realLinearIsometryEquiv_apply, OrderRingIso.toFun_eq_coe, RCLike.complexLinearIsometryEquiv_apply
toMonoidHom 📖	CompOp	4 math math: Rep.Action_ρ_eq_ρ, toMonoidHom_refl, FDRep.of_ρ, Rep.ihom_obj_ρ
toMulEquiv 📖	CompOp	1 math math: toMulEquiv_eq_coe
toNonUnitalRingHom 📖	CompOp	10 math math: toNonUnitalRingHom_injective, toNonUnitalRingHom_eq_coe, toNonUnitalRingHom_refl, symm_toNonUnitalRingHom_comp_toNonUnitalRingHom, nonUnitalSubsemiringMap_symm_apply_coe, toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply, symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply, nonUnitalSubsemiringMap_apply_coe, toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom, toNonUnitalRingHom_trans
toOpposite 📖	CompOp	3 math math: toOpposite_symm_apply, toOpposite_apply, AlgEquiv.toRingEquiv_toOpposite
toRingHom 📖	CompOp	43 math math: AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, NumberField.InfinitePlace.isometry_embedding, AddMonoidAlgebra.toRingHom_mapRangeRingEquiv, IsLocalization.isLocalization_iff_of_ringEquiv, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, AddMonoidAlgebra.toRingHom_mapDomainRingEquiv, ModuleCat.restrictScalars_isEquivalence_of_ringEquiv, RingHom.quotientKerEquivOfSurjective_symm_comp, IsLocalization.isLocalization_iff_of_base_ringEquiv, symm_toRingHom_comp_toRingHom, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, IsFractionRing.isFractionRing_iff_of_base_ringEquiv, symm_toRingHom_apply_toRingHom_apply, IsPerfectClosure.equiv_toRingHom, toRingHom_trans, MonoidAlgebra.toRingHom_mapDomainRingEquiv, evalRingHom_mapMatrix_comp_compRingEquiv, subsemiringMap_symm_apply_coe, Algebra.WeaklyQuasiFiniteAt.comap_algEquiv, PadicInt.toZMod_eq_residueField_comp_residue, PrimeSpectrum.comapEquiv_apply, LaurentSeries.powerSeries_ext_subring, IsLocalization.isLocalization_of_base_ringEquiv, NumberField.InfinitePlace.isometry_embedding_of_isReal, MvPolynomial.isEmptyRingEquiv_symm_toRingHom, toRingHom_refl, finite, Padic.isUniformInducing_cast_withVal, MonoidAlgebra.toRingHom_mapRangeRingEquiv, Padic.coe_withValRingEquiv_symm, toRingHom_apply_symm_toRingHom_apply, surjectiveOnStalks, toRingHom_eq_coe, TruncatedWittVector.commutes, toRingHom_injective, RingHom.ker_equiv_comp, toRingHom_comp_symm_toRingHom, Algebra.QuasiFiniteAt.comap_algEquiv, WittVector.zmodEquivTrunc_compat, AlgebraicGeometry.localRingHom_comp_stalkIso, IsPerfectClosure.equiv_symm_toRingHom, Padic.isDenseInducing_cast_withVal, TruncatedWittVector.commutes_symm
trans 📖	CompOp	29 math math: FractionalIdeal.canonicalEquiv_trans_canonicalEquiv, coe_ringHom_trans, OrderRingIso.trans_toRingEquiv_aux, iterateFrobeniusEquiv_symm_add, ZMod.ringEquivCongr_trans, MonoidAlgebra.mapDomainRingEquiv_trans, AddMonoidAlgebra.mapRangeRingEquiv_trans, toRingHom_trans, coe_mulEquiv_trans, OrderRingIso.trans_toRingEquiv, trans_apply, AddMonoidAlgebra.mapDomainRingEquiv_trans, symm_trans_self, IsPerfectClosure.equiv_comp_equiv_eq_id, MonoidAlgebra.mapRangeRingEquiv_trans, IsLocalRing.ResidueField.mapEquiv_trans, iterateFrobeniusEquiv_add, symm_trans_apply, symm_trans, MvPolynomial.mapEquiv_trans, coe_addEquiv_trans, coe_addMonoidHom_trans, coe_trans, coe_monoidHom_trans, IsPerfectClosure.equiv_comp_equiv, piCongrRight_trans, mapMatrix_trans, toNonUnitalRingHom_trans, self_trans_symm
unop 📖	CompOp	1 math math: AlgEquiv.toRingEquiv_unop

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
apply_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.apply_symm_apply
bijective 📖	mathematical	—	Function.Bijective DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.bijective
cast_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike cast	—	—
cast_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike symm cast	—	—
coe_addEquiv_refl 📖	mathematical	—	AddEquivClass.toAddEquiv RingEquiv instEquivLike RingEquivClass.toAddEquivClass instRingEquivClass refl AddEquiv.refl	—	RingEquivClass.toAddEquivClass instRingEquivClass
coe_addEquiv_trans 📖	mathematical	—	AddEquivClass.toAddEquiv RingEquiv instEquivLike RingEquivClass.toAddEquivClass instRingEquivClass trans AddEquiv.trans	—	RingEquivClass.toAddEquivClass instRingEquivClass
coe_addMonoidHom_refl 📖	mathematical	—	AddMonoidHomClass.toAddMonoidHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne EquivLike.toFunLike instEquivLike RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass instRingEquivClass refl AddMonoidHom.id	—	RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass instRingEquivClass
coe_addMonoidHom_trans 📖	mathematical	—	AddMonoidHomClass.toAddMonoidHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid EquivLike.toFunLike instEquivLike NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass instRingEquivClass trans AddMonoidHom.comp RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass	—	NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass instRingEquivClass
coe_mk 📖	mathematical	Equiv.toFun	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike Equiv Equiv.instEquivLike	—	—
coe_monoidHom_refl 📖	mathematical	—	MonoidHomClass.toMonoidHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass EquivLike.toFunLike instEquivLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass instRingEquivClass refl MonoidHom.id	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass instRingEquivClass
coe_monoidHom_trans 📖	mathematical	—	MonoidHomClass.toMonoidHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass EquivLike.toFunLike instEquivLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass instRingEquivClass trans MonoidHom.comp	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass instRingEquivClass
coe_mulEquiv_refl 📖	mathematical	—	MulEquivClass.toMulEquiv RingEquiv instEquivLike RingEquivClass.toMulEquivClass instRingEquivClass refl MulEquiv.refl	—	RingEquivClass.toMulEquivClass instRingEquivClass
coe_mulEquiv_trans 📖	mathematical	—	MulEquivClass.toMulEquiv RingEquiv instEquivLike RingEquivClass.toMulEquivClass instRingEquivClass trans MulEquiv.trans	—	RingEquivClass.toMulEquivClass instRingEquivClass
coe_nonUnitalRingHom_inj_iff 📖	mathematical	—	NonUnitalRingHomClass.toNonUnitalRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toNonUnitalRingHomClass instRingEquivClass	—	RingEquivClass.toNonUnitalRingHomClass instRingEquivClass ext NonUnitalRingHom.ext_iff
coe_ofBijective 📖	mathematical	Function.Bijective DFunLike.coe	RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike ofBijective	—	—
coe_prodCongr 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike prodCongr	—	—
coe_refl 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike refl	—	—
coe_ringHom_inj_iff 📖	mathematical	—	RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass	—	RingEquivClass.toRingHomClass instRingEquivClass ext RingHom.ext_iff
coe_ringHom_ofRingHom 📖	mathematical	RingHom.comp RingHom.id	RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass ofRingHom	—	RingEquivClass.toRingHomClass instRingEquivClass
coe_ringHom_refl 📖	mathematical	—	RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass refl RingHom.id	—	RingEquivClass.toRingHomClass instRingEquivClass
coe_ringHom_trans 📖	mathematical	—	RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass trans RingHom.comp	—	RingEquivClass.toRingHomClass instRingEquivClass
coe_toAddEquiv 📖	mathematical	—	DFunLike.coe AddEquiv EquivLike.toFunLike AddEquiv.instEquivLike AddEquivClass.toAddEquiv RingEquiv instEquivLike RingEquivClass.toAddEquivClass instRingEquivClass	—	RingEquivClass.toAddEquivClass instRingEquivClass
coe_toAddEquiv_symm 📖	mathematical	—	AddEquivClass.toAddEquiv RingEquiv instEquivLike RingEquivClass.toAddEquivClass instRingEquivClass symm AddEquiv.symm	—	RingEquivClass.toAddEquivClass instRingEquivClass
coe_toEquiv 📖	mathematical	—	DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike EquivLike.toEquiv RingEquiv instEquivLike	—	—
coe_toEquiv_symm 📖	mathematical	—	EquivLike.toEquiv RingEquiv instEquivLike symm Equiv.symm	—	—
coe_toMulEquiv 📖	mathematical	—	DFunLike.coe MulEquiv EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.toMulEquiv RingEquiv instEquivLike RingEquivClass.toMulEquivClass instRingEquivClass	—	RingEquivClass.toMulEquivClass instRingEquivClass
coe_toMulEquiv_symm 📖	mathematical	—	MulEquivClass.toMulEquiv RingEquiv instEquivLike RingEquivClass.toMulEquivClass instRingEquivClass symm MulEquiv.symm	—	RingEquivClass.toMulEquivClass instRingEquivClass
coe_toNonUnitalRingHom 📖	mathematical	—	DFunLike.coe NonUnitalRingHom NonUnitalRingHom.instFunLike NonUnitalRingHomClass.toNonUnitalRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toNonUnitalRingHomClass instRingEquivClass	—	RingEquivClass.toNonUnitalRingHomClass instRingEquivClass
coe_toRingHom 📖	mathematical	—	DFunLike.coe RingHom RingHom.instFunLike RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass	—	RingEquivClass.toRingHomClass instRingEquivClass
coe_trans 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike trans	—	—
comp_ofBijective_symm 📖	mathematical	Function.Bijective DFunLike.coe NonUnitalRingHom NonUnitalRingHom.instFunLike	NonUnitalRingHom.comp NonUnitalRingHomClass.toNonUnitalRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toNonUnitalRingHomClass instRingEquivClass symm ofBijective NonUnitalRingHom.instNonUnitalRingHomClass NonUnitalRingHom.id	—	NonUnitalRingHom.ext RingEquivClass.toNonUnitalRingHomClass instRingEquivClass NonUnitalRingHom.instNonUnitalRingHomClass injective apply_symm_apply
comp_symm 📖	mathematical	—	RingHom.comp RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass symm RingHom.id	—	RingHom.ext RingEquivClass.toRingHomClass instRingEquivClass apply_symm_apply
congr_arg 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	DFunLike.congr_arg
congr_fun 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	DFunLike.congr_fun
eq_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.eq_symm_apply
ext 📖	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	—	DFunLike.ext
ext_iff 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	ext
image_eq_preimage 📖	mathematical	—	Set.image DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike Set.preimage symm	—	image_eq_preimage_symm
image_eq_preimage_symm 📖	mathematical	—	Set.image DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike Set.preimage symm	—	Equiv.image_eq_preimage_symm
image_symm_eq_preimage 📖	mathematical	—	Set.image DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike symm Set.preimage	—	Equiv.image_symm_eq_preimage
injective 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.injective
instRingEquivClass 📖	mathematical	—	RingEquivClass RingEquiv instEquivLike	—	map_mul' map_add'
invFun_eq_symm 📖	mathematical	—	EquivLike.inv RingEquiv instEquivLike DFunLike.coe EquivLike.toFunLike symm	—	—
map_add 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	map_add AddEquivClass.instAddHomClass RingEquivClass.toAddEquivClass instRingEquivClass
map_add' 📖	mathematical	—	Equiv.toFun toEquiv	—	—
map_eq_neg_one_iff 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Distrib.toAdd EquivLike.toFunLike instEquivLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	neg_eq_iff_eq_neg map_neg RingHomClass.toAddMonoidHomClass RingEquivClass.toRingHomClass instRingEquivClass map_eq_one_iff
map_eq_one_iff 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	EmbeddingLike.map_eq_one_iff EquivLike.toEmbeddingLike MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass instRingEquivClass
map_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	EmbeddingLike.map_eq_zero_iff EquivLike.toEmbeddingLike AddMonoidHomClass.toZeroHomClass NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass instRingEquivClass
map_mul 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	map_mul MulEquivClass.instMulHomClass RingEquivClass.toMulEquivClass instRingEquivClass
map_mul' 📖	mathematical	—	Equiv.toFun toEquiv	—	—
map_ne_one_iff 📖	—	—	—	—	EmbeddingLike.map_ne_one_iff EquivLike.toEmbeddingLike MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass instRingEquivClass
map_ne_zero_iff 📖	—	—	—	—	EmbeddingLike.map_ne_zero_iff EquivLike.toEmbeddingLike AddMonoidHomClass.toZeroHomClass NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass instRingEquivClass
map_neg 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup	—	map_neg NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass instRingEquivClass
map_neg_one 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Distrib.toAdd EquivLike.toFunLike instEquivLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	map_neg map_one
map_one 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass instRingEquivClass
map_pow 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingEquivClass.toRingHomClass instRingEquivClass
map_sub 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike SubNegMonoid.toSub AddGroup.toSubNegMonoid AddCommGroup.toAddGroup NonUnitalNonAssocRing.toAddCommGroup	—	map_sub NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass instRingEquivClass
map_zero 📖	mathematical	—	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	map_zero AddMonoidHomClass.toZeroHomClass NonUnitalRingHomClass.toAddMonoidHomClass RingEquivClass.toNonUnitalRingHomClass instRingEquivClass
mk_coe 📖	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike Equiv.toFun	—	—	ext
mk_coe' 📖	mathematical	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike Equiv.toFun	symm	—	Function.Bijective.injective symm_bijective ext
ofBijective_apply 📖	mathematical	Function.Bijective DFunLike.coe	RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike ofBijective	—	—
ofBijective_symm_comp 📖	mathematical	Function.Bijective DFunLike.coe NonUnitalRingHom NonUnitalRingHom.instFunLike	NonUnitalRingHom.comp NonUnitalRingHomClass.toNonUnitalRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toNonUnitalRingHomClass instRingEquivClass symm ofBijective NonUnitalRingHom.instNonUnitalRingHomClass NonUnitalRingHom.id	—	NonUnitalRingHom.ext RingEquivClass.toNonUnitalRingHomClass instRingEquivClass NonUnitalRingHom.instNonUnitalRingHomClass injective apply_symm_apply
ofHomInv'_apply 📖	mathematical	NonUnitalRingHom.comp NonUnitalRingHom.id	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike ofNonUnitalRingHom NonUnitalRingHom NonUnitalRingHom.instFunLike	—	ofNonUnitalRingHom_apply
ofHomInv'_symm_apply 📖	mathematical	NonUnitalRingHom.comp NonUnitalRingHom.id	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike symm ofNonUnitalRingHom NonUnitalRingHom NonUnitalRingHom.instFunLike	—	ofNonUnitalRingHom_symm_apply
ofHomInv_apply 📖	mathematical	RingHom.comp RingHom.id	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike ofRingHom RingHom RingHom.instFunLike	—	ofRingHom_apply
ofHomInv_symm_apply 📖	mathematical	RingHom.comp RingHom.id	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike symm ofRingHom RingHom RingHom.instFunLike	—	ofRingHom_symm_apply
ofNonUnitalRingHom_apply 📖	mathematical	NonUnitalRingHom.comp NonUnitalRingHom.id	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike ofNonUnitalRingHom NonUnitalRingHom NonUnitalRingHom.instFunLike	—	—
ofNonUnitalRingHom_symm_apply 📖	mathematical	NonUnitalRingHom.comp NonUnitalRingHom.id	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike symm ofNonUnitalRingHom NonUnitalRingHom NonUnitalRingHom.instFunLike	—	—
ofRingHom_apply 📖	mathematical	RingHom.comp RingHom.id	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike ofRingHom RingHom RingHom.instFunLike	—	—
ofRingHom_coe_ringHom 📖	mathematical	RingHom.comp RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass RingHom.id	ofRingHom	—	RingEquivClass.toRingHomClass instRingEquivClass ext
ofRingHom_symm 📖	mathematical	RingHom.comp RingHom.id	symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd ofRingHom	—	—
ofRingHom_symm_apply 📖	mathematical	RingHom.comp RingHom.id	DFunLike.coe RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike symm ofRingHom RingHom RingHom.instFunLike	—	—
opOp_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite MulOpposite.instMul MulOpposite.instAdd EquivLike.toFunLike instEquivLike opOp MulOpposite.op	—	—
opOp_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite MulOpposite.instMul MulOpposite.instAdd EquivLike.toFunLike instEquivLike symm opOp MulOpposite.unop	—	—
op_apply_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite MulOpposite.instMul MulOpposite.instAdd EquivLike.toFunLike instEquivLike Equiv Equiv.instEquivLike op MulOpposite.op MulOpposite.unop	—	—
op_apply_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite MulOpposite.instMul MulOpposite.instAdd EquivLike.toFunLike instEquivLike symm Equiv Equiv.instEquivLike op MulOpposite.op AddEquiv AddEquiv.instEquivLike AddEquiv.symm AddEquivClass.toAddEquiv RingEquivClass.toAddEquivClass instRingEquivClass MulOpposite.unop	—	—
op_symm_apply_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike Equiv MulOpposite MulOpposite.instMul MulOpposite.instAdd Equiv.instEquivLike Equiv.symm op MulOpposite.unop MulOpposite.op	—	—
op_symm_apply_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike symm Equiv MulOpposite MulOpposite.instMul MulOpposite.instAdd Equiv.instEquivLike Equiv.symm op MulOpposite.unop AddEquiv AddEquiv.instEquivLike AddEquiv.symm AddEquivClass.toAddEquiv RingEquivClass.toAddEquivClass instRingEquivClass MulOpposite.op	—	—
piCongrLeft'_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Pi.instAdd Distrib.toAdd instEquivLike piCongrLeft'	—	—
piCongrLeft'_symm 📖	mathematical	—	symm Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instAdd Distrib.toAdd piCongrLeft' Equiv.symm	—	MulEquiv.map_mul' MulEquiv.symm_map_mul Equiv.piCongrLeft'_symm AddEquiv.map_add'
piCongrLeft'_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instAdd Distrib.toAdd instEquivLike symm piCongrLeft' Equiv.symm_apply_apply	—	—
piCongrLeft_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Equiv EquivLike.toFunLike Equiv.instEquivLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instAdd Distrib.toAdd instEquivLike piCongrLeft MulEquiv MulEquiv.instEquivLike MulEquiv.symm MulEquivClass.toMulEquiv RingEquivClass.toMulEquivClass instRingEquivClass piCongrLeft' Equiv.symm	—	—
piCongrLeft_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Equiv EquivLike.toFunLike Equiv.instEquivLike Pi.instAdd Distrib.toAdd instEquivLike symm piCongrLeft piCongrLeft' Equiv.symm	—	—
piCongrRight_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike piCongrRight	—	—
piCongrRight_refl 📖	mathematical	—	piCongrRight refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd Pi.instMul Pi.instAdd	—	—
piCongrRight_symm 📖	mathematical	—	symm Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instAdd Distrib.toAdd piCongrRight	—	—
piCongrRight_trans 📖	mathematical	—	trans Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instAdd Distrib.toAdd piCongrRight	—	—
piEquivPiSubtypeProd_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Prod.instMul Pi.instAdd Distrib.toAdd Prod.instAdd EquivLike.toFunLike instEquivLike piEquivPiSubtypeProd	—	—
piEquivPiSubtypeProd_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Prod.instAdd Pi.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike symm piEquivPiSubtypeProd	—	—
piOptionEquivProd_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Prod.instMul Pi.instAdd Distrib.toAdd Prod.instAdd EquivLike.toFunLike instEquivLike piOptionEquivProd	—	—
piOptionEquivProd_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instMul Prod.instAdd Distrib.toAdd Pi.instAdd EquivLike.toFunLike instEquivLike symm piOptionEquivProd	—	—
piUnique_apply 📖	mathematical	—	DFunLike.coe RingEquiv Unique.instInhabited Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike piUnique	—	—
piUnique_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Unique.instInhabited Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Pi.instMul Distrib.toAdd Pi.instAdd EquivLike.toFunLike instEquivLike symm piUnique uniqueElim	—	—
prodCongr_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike prodCongr	—	—
prodCongr_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Prod.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike symm prodCongr Equiv Equiv.instEquivLike Equiv.symm EquivLike.toEquiv	—	—
refl_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike refl	—	—
self_trans_symm 📖	mathematical	—	trans symm refl	—	ext Equiv.left_inv
sumArrowEquivProdArrow_apply 📖	mathematical	—	DFunLike.coe RingEquiv Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instMul Pi.instAdd Distrib.toAdd Prod.instAdd EquivLike.toFunLike instEquivLike sumArrowEquivProdArrow Equiv Equiv.instEquivLike Equiv.sumArrowEquivProdArrow	—	—
sumArrowEquivProdArrow_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv Prod.instMul Pi.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Prod.instAdd Pi.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike symm sumArrowEquivProdArrow Equiv Equiv.instEquivLike Equiv.symm Equiv.sumArrowEquivProdArrow	—	—
surjective 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike	—	EquivLike.surjective
symm_apply_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_apply_apply
symm_apply_eq 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike symm	—	Equiv.symm_apply_eq
symm_bijective 📖	mathematical	—	Function.Bijective RingEquiv symm	—	Function.bijective_iff_has_inverse symm_symm
symm_comp 📖	mathematical	—	RingHom.comp RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass symm RingHom.id	—	RingHom.ext RingEquivClass.toRingHomClass instRingEquivClass symm_apply_apply
symm_mk 📖	mathematical	Equiv.toFun	symm	—	—
symm_ofNonUnitalRingHom 📖	mathematical	NonUnitalRingHom.comp NonUnitalRingHom.id	symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd ofNonUnitalRingHom	—	—
symm_refl 📖	mathematical	—	symm refl	—	—
symm_symm 📖	mathematical	—	symm	—	—
symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply 📖	mathematical	—	DFunLike.coe NonUnitalRingHom NonUnitalRingHom.instFunLike toNonUnitalRingHom symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd	—	Equiv.symm_apply_apply
symm_toNonUnitalRingHom_comp_toNonUnitalRingHom 📖	mathematical	—	NonUnitalRingHom.comp toNonUnitalRingHom symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd NonUnitalRingHom.id	—	NonUnitalRingHom.ext symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply
symm_toRingHom_apply_toRingHom_apply 📖	mathematical	—	DFunLike.coe RingHom RingHom.instFunLike toRingHom symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd	—	Equiv.symm_apply_apply
symm_toRingHom_comp_toRingHom 📖	mathematical	—	RingHom.comp toRingHom symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd RingHom.id	—	symm_comp
symm_trans 📖	mathematical	—	symm trans	—	—
symm_trans_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike symm trans	—	—
symm_trans_self 📖	mathematical	—	trans symm refl	—	ext Equiv.right_inv
toAddEquiv_eq_coe 📖	mathematical	—	toAddEquiv AddEquivClass.toAddEquiv RingEquiv instEquivLike RingEquivClass.toAddEquivClass instRingEquivClass	—	—
toAddMonoidHom_refl 📖	mathematical	—	toAddMonoidHom refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd AddMonoidHom.id AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	—
toAddMonoidMom_commutes 📖	mathematical	—	RingHom.toAddMonoidHom RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass AddEquiv.toAddMonoidHom AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne AddEquivClass.toAddEquiv RingEquivClass.toAddEquivClass	—	RingEquivClass.toRingHomClass instRingEquivClass
toEquiv_commutes 📖	mathematical	—	AddEquiv.toEquiv Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddEquivClass.toAddEquiv RingEquiv Distrib.toMul instEquivLike RingEquivClass.toAddEquivClass instRingEquivClass MulEquiv.toEquiv MulEquivClass.toMulEquiv RingEquivClass.toMulEquivClass	—	RingEquivClass.toAddEquivClass instRingEquivClass
toEquiv_eq_coe 📖	mathematical	—	toEquiv EquivLike.toEquiv RingEquiv instEquivLike	—	—
toMonoidHom_commutes 📖	mathematical	—	RingHom.toMonoidHom RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass MulEquiv.toMonoidHom MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass MulEquivClass.toMulEquiv RingEquivClass.toMulEquivClass	—	RingEquivClass.toRingHomClass instRingEquivClass
toMonoidHom_refl 📖	mathematical	—	toMonoidHom refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd MonoidHom.id MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass	—	—
toMulEquiv_eq_coe 📖	mathematical	—	toMulEquiv MulEquivClass.toMulEquiv RingEquiv instEquivLike RingEquivClass.toMulEquivClass instRingEquivClass	—	—
toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply 📖	mathematical	—	DFunLike.coe NonUnitalRingHom NonUnitalRingHom.instFunLike toNonUnitalRingHom symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd	—	Equiv.apply_symm_apply
toNonUnitalRingHom_commutes 📖	mathematical	—	NonUnitalRingHomClass.toNonUnitalRingHom RingHom NonAssocSemiring.toNonUnitalNonAssocSemiring RingHom.instFunLike RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass RingEquivClass.toNonUnitalRingHomClass	—	RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass RingEquivClass.toRingHomClass instRingEquivClass
toNonUnitalRingHom_eq_coe 📖	mathematical	—	toNonUnitalRingHom NonUnitalRingHomClass.toNonUnitalRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toNonUnitalRingHomClass instRingEquivClass	—	—
toNonUnitalRingHom_injective 📖	mathematical	—	RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd NonUnitalRingHom toNonUnitalRingHom	—	ext NonUnitalRingHom.ext_iff
toNonUnitalRingHom_refl 📖	mathematical	—	toNonUnitalRingHom refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd NonUnitalRingHom.id	—	—
toNonUnitalRingHom_trans 📖	mathematical	—	toNonUnitalRingHom trans Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd NonUnitalRingHom.comp	—	—
toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom 📖	mathematical	—	NonUnitalRingHom.comp toNonUnitalRingHom symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd NonUnitalRingHom.id	—	NonUnitalRingHom.ext toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply
toOpposite_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring MulOpposite.instMul Distrib.toAdd MulOpposite.instAdd EquivLike.toFunLike instEquivLike toOpposite MulOpposite.op	—	—
toOpposite_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite MulOpposite.instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalSemiring.toNonUnitalNonAssocSemiring NonUnitalCommSemiring.toNonUnitalSemiring MulOpposite.instAdd Distrib.toAdd EquivLike.toFunLike instEquivLike symm toOpposite MulOpposite.unop	—	—
toRingHom_apply_symm_toRingHom_apply 📖	mathematical	—	DFunLike.coe RingHom RingHom.instFunLike toRingHom symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd	—	Equiv.apply_symm_apply
toRingHom_comp_symm_toRingHom 📖	mathematical	—	RingHom.comp toRingHom symm Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd RingHom.id	—	comp_symm
toRingHom_eq_coe 📖	mathematical	—	toRingHom RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike instEquivLike RingEquivClass.toRingHomClass instRingEquivClass	—	—
toRingHom_injective 📖	mathematical	—	RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd RingHom toRingHom	—	ext RingHom.ext_iff
toRingHom_refl 📖	mathematical	—	toRingHom refl Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd RingHom.id	—	—
toRingHom_trans 📖	mathematical	—	toRingHom trans Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd RingHom.comp	—	—
trans_apply 📖	mathematical	—	DFunLike.coe RingEquiv EquivLike.toFunLike instEquivLike trans	—	—

RingEquiv.Simps

Definitions

Name	Category	Theorems
symm_apply 📖	CompOp	—

RingEquiv.symm_mk

Definitions

Name	Category	Theorems
aux 📖	CompOp	—

RingEquivClass

Definitions

Name	Category	Theorems
toRingEquiv 📖	CompOp	40 math math: AlgEquiv.coe_restrictScalars_symm, OrderRingIso.trans_toRingEquiv_aux, AlgEquiv.toRingEquiv_toRingHom, PowerBasis.quotientEquivQuotientMinpolyMap_apply, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, StarRingEquiv.toRingEquiv_eq_coe, DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv, OrderRingIso.toRingEquiv_eq_coe, BialgEquiv.toRingEquiv_toRingHom, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, OrderRingIso.coe_ringEquiv_refl, AlgEquiv.op_apply_symm_apply, StarAlgEquiv.toRingEquiv_symm, AlgEquiv.coe_ringEquiv_injective, StarAlgEquiv.symm_to_ringEquiv, StarAlgEquiv.toRingEquiv_eq_coe, AlgEquiv.coe_ringEquiv, AlgEquiv.toRingEquiv_opOp, AlgEquiv.op_symm_apply_symm_apply, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, AlgEquiv.coe_restrictScalars, IsLocalization.algEquivOfAlgEquiv_symm_apply, AlgEquiv.opComm_apply_symm_apply, RingInvo.coe_ringEquiv, DoubleQuot.quotQuotEquivCommₐ_toRingEquiv, DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv, AlgEquiv.opComm_symm_apply_symm_apply, DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv, AlgEquiv.toRingEquiv_toOpposite, StarAlgEquiv.to_ringEquiv_symm, AlgEquiv.symm_toRingEquiv, MulSemiringAction.toRingEquiv_algEquiv, AlgEquiv.subalgebraMap_symm_apply_coe, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, AlgEquiv.toRingEquiv_symm, Rat.ringOfIntegersWithValEquiv_apply, OrderRingIso.coe_toRingEquiv, AlgEquiv.coe_ringHom_commutes, AlgEquiv.toRingEquiv_eq_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
map_add 📖	mathematical	—	DFunLike.coe EquivLike.toFunLike	—	—
toAddEquivClass 📖	mathematical	—	AddEquivClass	—	map_add
toMulEquivClass 📖	mathematical	—	MulEquivClass	—	—
toNonUnitalRingHomClass 📖	mathematical	—	NonUnitalRingHomClass EquivLike.toFunLike	—	MulEquivClass.map_mul toMulEquivClass map_add map_zero AddMonoidHomClass.toZeroHomClass AddEquivClass.instAddMonoidHomClass toAddEquivClass
toRingHomClass 📖	mathematical	—	RingHomClass EquivLike.toFunLike	—	MulEquivClass.map_mul toMulEquivClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass MulEquivClass.toMonoidWithZeroHomClass map_add map_zero MonoidWithZeroHomClass.toZeroHomClass

RingHom

Definitions

Name	Category	Theorems
inverse 📖	CompOp	1 math math: inverse_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
inverse_apply 📖	mathematical	DFunLike.coe RingHom instFunLike	inverse	—	—

(root)

Definitions

Name	Category	Theorems
RingEquivClass 📖	CompData	7 math math: RingEquiv.instRingEquivClass, AlgEquivClass.toRingEquivClass, StarRingEquiv.instRingEquivClass, OrderRingIso.instRingEquivClass, NonUnitalAlgEquivClass.toRingEquivClass, RingInvoClass.toRingEquivClass, StarRingEquivClass.toRingEquivClass
instCoeTCRingEquivOfRingEquivClass 📖	CompOp	—
«term_≃+*_» 📖	CompOp	—

---

← Back to Index