RingEquiv 📖 | CompData | 718 mathmath: MonoidAlgebra.mapDomainRingEquiv_single, AbsoluteValue.IsEquiv.isEmbedding_equivWithAbs, RingEquiv.piCongrRight_apply, RCLike.sqrt_eq_ite, AddMonoidAlgebra.mapDomainRingEquiv_apply, RingEquiv.apply_symm_apply, RingEquiv.restrict_symm_apply_coe, RingEquiv.toRingCatIso_inv, RingEquiv.coe_ringHom_trans, Language.reverseIso_apply, Polynomial.roots_expand, RingEquiv.toOpposite_symm_apply, FractionalIdeal.mapEquiv_apply, AlgebraicGeometry.StructureSheaf.globalSectionsIso_inv, RingAut.one_eq_refl, Int.quotientSpanEquivZMod_comp_Quotient_mk, RingEquiv.toNonUnitalRingHom_injective, frobeniusEquiv_apply, BitVec.equivFin_symm_apply_toFin, RingEquiv.coe_addEquiv_refl, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_apply_mk, iterateFrobeniusEquiv_symm_add_apply, coe_frobeniusEquiv_symm_comp_coe_frobenius, RingEquiv.coe_prodComm_symm, RingEquiv.surjective, RingEquiv.ofHomInv'_apply, RingHom.IsStandardSmoothOfRelativeDimension.equiv, RingEquiv.op_apply_apply, Ideal.quotientEquiv_symm_apply, RingEquiv.idealComapOrderIso_apply, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply, IsPerfectClosure.equiv_comp_equiv_apply_eq_self, RingEquiv.asBoolRingAsBoolAlg_apply, MvPolynomial.isEmptyRingEquiv_apply, Polynomial.opRingEquiv_op_monomial, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm, FDRep.endRingEquiv_symm_comp_ρ, RingEquiv.toOpposite_apply, RingEquiv.map_sub, BoolRing.Iso.mk_hom_hom', Algebra.trace_eq_of_ringEquiv, LaurentSeries.LaurentSeriesRingEquiv_def, RingEquiv.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, RingEquiv.prodProdProdComm_apply, Ideal.comap_symm, AlgEquiv.coe_ringEquiv', RingEquiv.map_list_sum, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_mk, Int.quotientSpanNatEquivZMod_comp_Quotient_mk, RingEquiv.map_neg, cyclotomicCharacter.toZModPow, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, NonUnitalSubsemiring.coe_equivMapOfInjective_apply, NumberField.FinitePlace.embedding_apply, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, 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, Perfection.coeff_iterate_symm_frobeniusEquiv, RingEquiv.ofRingHom_coe_ringHom, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, rootsOfUnity.integer_power_of_ringEquiv, Polynomial.leadingCoeff_opRingEquiv, RingEquiv.toCommSemiRingCatIso_inv, Subring.centerCongr_apply_coe, RingEquiv.mopMatrix_symm_apply, NonUnitalSubsemiring.centerCongr_symm_apply_coe, RingEquiv.ofLeftInverse_symm_apply, NumberField.InfinitePlace.Completion.norm_coe, iterateFrobeniusEquiv_def, RingEquiv.piOptionEquivProd_apply, RingEquiv.op_apply_symm_apply, RingCon.comapQuotientEquivRange_symm_mk, RingEquiv.piCongrLeft_symm_apply, RingEquiv.ofLeftInverse_apply, RingEquiv.snd_comp_coe_prodComm, RCLike.realRingEquiv_symm_apply, IsGaloisGroup.ringEquivFixedPoints_apply_coe, MonoidAlgebra.mapRingEquiv_single, Ring.DirectLimit.congr_symm_apply_of, BoolRing.Iso.mk_inv_hom', RingCon.comapQuotientEquivOfSurj_symm_mk, RingEquiv.ext_iff, RingEquiv.piCongrLeft'_apply, Perfection.coe_pthRoot_eq_symm_frobeniusEquiv, NonUnitalSubring.centerCongr_apply_coe, RingEquiv.ofHomInv_symm_apply, RingEquiv.mopMatrix_apply, Subsemiring.centerCongr_symm_apply_coe, MonoidAlgebra.opRingEquiv_symm_apply, NumberField.RingOfIntegers.withValEquiv_symm_apply, Matrix.uniqueRingEquiv_apply, RingEquiv.coe_toMulEquiv, ModuleCat.endRingEquiv_symm_apply_hom, RingEquiv.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, RingCon.comapQuotientEquivOfSurj_symm_mk', RingEquiv.ofLeftInverseS_symm_apply, AddMonoidAlgebra.opRingEquiv_symm_apply, Valuation.IsEquiv.uniformContinuous_equiv, IsSimpleRing.exists_ringEquiv_matrix_end_mulOpposite, MulSemiringAction.toRingEquiv_apply, NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe, modularCyclotomicCharacter.toFun_spec', RingEquiv.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, RingEquiv.asBoolRingAsBoolAlg_symm_apply, DoubleQuot.quotQuotEquivComm_quotQuotMk, HahnSeries.toMvPowerSeries_symm_apply_coeff, RingEquiv.toNonUnitalRingHom_commutes, PreTilt.coeff_frobeniusEquiv_symm, DividedPowers.ofRingEquiv_dpow, DividedPowers.equiv_apply, RingCon.comapQuotientEquivRangeS_symm_mk, IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv_symm_apply, Ideal.spanRank_map_eq_of_ringEquiv, RingEquiv.moduleEndSelf_symm_apply, Matrix.transposeRingEquiv_symm_apply, Ideal.lift_spanRank_map_eq_of_ringEquiv, Subsemiring.coe_equivMapOfInjective_apply, starRingAut_apply, Perfection.coeff_symm_frobeniusEquiv, Matrix.piRingEquiv_apply, NonUnitalSubring.topEquiv_symm_apply_coe, isSemisimpleRing_iff_pi_matrix_divisionRing, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, RingEquiv.instRingEquivClass, Polynomial.opRingEquiv_op_C, RingEquiv.coe_ofBijective, Polynomial.roots_X_pow_char_pow_sub_C_pow, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, iterateFrobeniusEquiv_add_apply, WithVal.congr_symm_apply, IsLocalization.ringEquivOfRingEquiv_symm_apply, RingEquiv.symm_apply_apply, iterateFrobeniusEquiv_eq_pow, RingEquiv.sofLeftInverse'_apply, RingHomInvPair.toRingEquiv_symm_apply, RingEquiv.mk_coe, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, RingAut.one_apply, RingEquiv.map_neg_one, WithAbs.congr_symm_apply, RingEquiv.cast_apply, WithVal.val_apply_equiv, NumberField.AdeleRing.algebraMap_snd_apply, gelfandStarTransform_symm_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, Matrix.piRingEquiv_symm_apply, WithAbs.tendsto_one_div_one_add_pow_nhds_one, RingCon.comapQuotientEquivRange_mk, RingEquiv.symm_apply_eq, AlgEquiv.op_apply_symm_apply, IsDedekindDomain.HeightOneSpectrum.coe_algebraMap_mem, RingEquiv.piEquivPiSubtypeProd_symm_apply, IsAlgClosed.ringEquiv_of_equiv_of_char_eq, RingEquiv.quotientBot_mk, Algebra.norm_eq_of_equiv_equiv, RingEquiv.prodZeroRing_symm_apply, RingEquiv.ofBijective_apply, Subring.comap_equiv_eq_map_symm, WithVal.equiv_symm_apply, RingEquiv.zeroRingProd_symm_apply, Valuation.IsEquiv.uniformContinuous_equivWithVal, RingEquiv.map_one, RingEquiv.injective, RingEquiv.map_eq_zero_iff, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, MonoidAlgebra.toRingHom_mapRingEquiv, RingEquiv.map_zero, MvPolynomial.mapEquiv_apply, WittVector.IsocrystalEquiv.frob_equivariant, Subsemiring.centerCongr_apply_coe, AlgEquiv.coe_ringEquiv_injective, RingEquiv.map_eq_one_iff, Ideal.quotientEquiv_symm_mk, modularCyclotomicCharacter.toFun_spec, coe_ringEquiv_lpBCF, NonUnitalSubring.topEquiv_apply, NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal_coe, RingEquiv.toCommRingCatIso_inv, RingEquiv.toAddMonoidMom_commutes, FractionalIdeal.canonicalEquiv_mk0, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, RingEquiv.moduleEndSelfOp_apply, AdjoinRoot.quotEquivQuotMap_apply, RingEquiv.congr_arg, Subring.centerToMulOpposite_symm_apply_coe, RingEquiv.toRingCatIso_hom, Subsemiring.mem_map_equiv, RingEquiv.coe_toAddEquiv, Ring.DirectLimit.congr_apply_of, ZMod.ringEquivCongr_refl_apply, Subring.topEquiv_apply, RingEquiv.subsemiringMap_apply_coe, WithVal.equiv_apply, RingEquiv.coe_mk, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', 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', RingEquiv.invFun_eq_symm, RingEquiv.piEquivPiSubtypeProd_apply, Valuation.IsEquiv.uniformContinuous_congr, IsPrecomplete.congr_ringEquiv, RingEquiv.map_add, RingEquiv.toCommRingCatIso_hom, CategoryTheory.Iso.ringCatIsoToRingEquiv_toRingHom, MonoidAlgebra.opRingEquiv_symm_single, IsAlgClosed.ringEquiv_of_equiv_of_charZero, IsLocalization.ringEquivOfRingEquiv_eq_map, PreTilt.coeff_iterate_frobeniusEquiv_symm, IsLocalRing.ResidueField.mapEquiv_apply, DoubleQuot.coe_quotQuotEquivQuotSupₐ, Ideal.quotientMulEquivQuotientProd_snd, AddMonoidAlgebra.commRingEquiv_single_single, IsDecompositionField.algebraMap_ringEquiv_symm_apply, Module.End.ringEquivEndFinsupp_apply_apply_apply, RingEquiv.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, RingEquiv.moduleEndSelf_apply, Ideal.fst_comp_quotientMulEquivQuotientProd, RingEquiv.ofHomInv_apply, ZMod.ringEquivCongr_ringEquivCongr_apply, RingHomInvPair.toRingEquiv_apply, NonUnitalSubring.centerCongr_symm_apply_coe, Subsemiring.centerToMulOpposite_apply_coe, IsAlgClosure.equivOfEquiv_comp_algebraMap, RingEquiv.coe_addMonoidHom_refl, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_symm_mk, Submodule.equivOpposite_apply, RingCon.quotientQuotientEquivQuotient_coe_coe, MonoidAlgebra.curryRingEquiv_symm_single, RingEquiv.ofRingHom_symm_apply, AlgEquiv.toRingEquiv_unop, RingEquiv.coe_mulEquiv_trans, AbsoluteValue.IsEquiv.equivWithAbs_image_mem_nhds_zero, Int.quotientSpanEquivZMod_comp_castRingHom, RingCon.quotientKerEquivOfRightInverse_apply, IsGaloisGroup.algebraMap_ringEquiv_symm_apply, Matrix.transposeRingEquiv_apply, AlgEquiv.ofRingEquiv_apply, RingEquiv.prodCongr_apply, OrderRingIso.coe_mk, LocallyConstant.congrLeftRingEquiv_symm_apply_apply, frobeniusEquiv_symm_pow, IsSemisimpleRing.exists_ringEquiv_pi_matrix_divisionRing, evalRingHom_mapMatrix_comp_compRingEquiv, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, RingEquiv.map_det, LinearEquiv.conjRingEquiv_apply_apply, RingEquiv.subsemiringMap_symm_apply_coe, RingCon.comapQuotientEquivRangeS_mk, RingEquiv.trans_apply, coe_frobeniusEquiv, RingEquiv.coe_ringHom_inj_iff, addMonoidEndRingEquivInt_apply, quotAdjoinEquivQuotMap_apply_mk, RingEquiv.mapTwoSidedIdeal_apply, MulSemiringAction.toAlgEquiv_toEquiv, WittVector.dvd_sub_sum_teichmuller_iterateFrobeniusEquiv_coeff, LaurentSeries.coe_X_compare, FractionalIdeal.canonicalEquiv_coeIdeal, RingEquiv.toNonUnitalRingHom_eq_coe, frobenius_comp_frobeniusEquiv_symm, PerfectionMap.comp_equiv', iterateFrobeniusEquiv_symm, RingEquiv.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, RingEquiv.coe_nonUnitalRingHom_inj_iff, RingEquiv.idealComapOrderIso_symm_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, IsPerfectClosure.equiv_comp, Rat.HeightOneSpectrum.natGenerator_dvd_iff, RingEquiv.comp_ofBijective_symm, Polynomial.roots_X_pow_char_sub_C_pow, WittVector.inv_pair₂, DividedPowers.equiv_apply', Subring.centerToMulOpposite_apply_coe, WittVector.exists_frobenius_solution_fractionRing, MulSemiringAction.toRingEquiv_symm_apply, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.continuous_coe', Ideal.quotEquivOfEq_eq_factor, coe_frobenius_comp_coe_frobeniusEquiv_symm, AlgEquiv.op_symm_apply_symm_apply, FractionalIdeal.coeFun_mapEquiv, RingEquiv.coe_toEquiv, AddMonoidAlgebra.toRingHom_mapRingEquiv, RingEquiv.sumArrowEquivProdArrow_symm_apply, Ring.DirectLimit.ringEquiv_of, RingEquiv.symm_bijective, modularCyclotomicCharacter.unique, RingHom.quotientKerEquivOfRightInverse.Symm.apply, IsLocalization.AtPrime.equivQuotMaximalIdeal_apply_mk, RingEquiv.height_comap, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, RingCon.congr_mk, IsHausdorff.congr_ringEquiv, FractionalIdeal.canonicalEquiv_canonicalEquiv, RingEquiv.map_prod, MonoidAlgebra.mapRingEquiv_apply, WittVector.inv_pair₁, RingEquiv.restrict_apply_coe, Matrix.conjTransposeRingEquiv_symm_apply, IsDecompositionField.algebraMap_ringEquiv_apply, MonoidAlgebra.mapRangeRingEquiv_apply, RingEquiv.cast_symm_apply, RingEquiv.map_pow, RingEquiv.prodZeroRing_apply, RingHom.quotientKerEquivOfSurjective_apply_mk, Subsemiring.mopRingEquivOp_apply_coe, IsLocalization.AtPrime.algebraMap_equivQuotMaximalIdeal_symm_apply, IsPerfectClosure.equiv_self_apply, RingEquiv.toEquiv_eq_coe, PerfectionMap.comp_equiv, RingEquiv.piUnique_symm_apply, Ideal.pointwise_smul_eq_comap, RingEquiv.mapMatrix_apply, Ideal.snd_comp_quotientMulEquivQuotientProd, HahnSeries.coeff_toPowerSeries, RingHom.map_iterate_frobeniusEquiv_symm, AddMonoidAlgebra.mapRingEquiv_apply, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, RestrictScalars.ringEquiv_map_smul, frobeniusEquiv_def, Padic.toEquiv_withValUniformEquiv_eq_toEquiv_withValRingEquiv, Ideal.quotientEquiv_apply, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, Ideal.quotientInfEquivQuotientProd_snd, Polynomial.opRingEquiv_symm_C_mul_X_pow, RingEquiv.coe_prodComm, RingEquiv.toMonoidHom_commutes, NumberField.InfinitePlace.Completion.extensionEmbedding_coe, Polynomial.opRingEquiv_symm_monomial, RingEquiv.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, WithAbs.congr_apply, RCLike.complexRingEquiv_symm_apply, RingEquiv.ofLeftInverse'_symm_apply, WithAbs.equivWithAbs_equiv_symm_apply, RingEquiv.prodProdProdComm_toMulEquiv, FractionalIdeal.canonicalEquiv_flip, IsLocalization.isLocalization_of_base_ringEquiv, IsSemisimpleModule.exists_end_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, DividedPowers.ofRingEquiv_dpow_apply, LaurentSeries.powerSeriesRingEquiv_coe_apply, IsPerfectClosure.equiv_apply, Matrix.uniqueRingEquiv_symm_apply, IsAlgClosure.equivOfEquiv_symm_comp_algebraMap, RingEquiv.height_map, NumberField.InfinitePlace.isReal_comap_iff, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, LaurentSeries.powerSeriesEquivSubring_apply, RingEquiv.piCongrLeft_apply, iterate_frobeniusEquiv_symm_pow_p_pow, RingEquiv.toSemilinearEquiv_symm_apply, NonUnitalSubring.centerToMulOpposite_symm_apply_coe, Ideal.map_of_equiv, RingAut.inv_apply, RingEquiv.op_symm_apply_symm_apply, AlgEquiv.toRingEquiv_op, RingEquiv.nonUnitalSubsemiringMap_symm_apply_coe, AddMonoidAlgebra.curryRingEquiv_symm_single, RingEquiv.image_eq_preimage, AddMonoidAlgebra.opRingEquiv_apply, NonUnitalSubring.coe_equivMapOfInjective_apply, RingEquiv.ofLeftInverse'_apply, AddMonoidAlgebra.mapDomainRingEquiv_single, MonoidAlgebra.curryRingEquiv_single, WittVector.StandardOneDimIsocrystal.frobenius_apply, Subring.centerCongr_symm_apply_coe, WithVal.congr_apply, polynomial_expand_eq, RingEquiv.coe_toEquiv_symm, iterateFrobeniusEquiv_apply, IsAdicComplete.congr_ringEquiv, NonUnitalSubring.mem_map_equiv, Ideal.quotientMulEquivQuotientProd_fst, RingEquiv.toAddEquiv_eq_coe, IsAlgClosure.equivOfEquiv_algebraMap, IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_divisionRing, 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, RingEquiv.symm_trans_apply, RingEquiv.congr_fun, Polynomial.coeff_opRingEquiv, Ideal.map_symm, IsPerfectClosure.equiv_comp_apply, RingEquiv.mk_coe', WittVector.quotientPEquiv_mk, NumberField.RingOfIntegers.mapRingEquiv_apply, LocallyConstant.congrRightRingEquiv_symm_apply_apply, Polynomial.toFinsuppIso_apply, AddMonoidAlgebra.uniqueRingEquiv_symm_apply, Subsemiring.ringEquivOpMop_symm_apply_coe, RingEquiv.ofNonUnitalRingHom_symm_apply, LaurentSeries.powerSeriesEquivSubring_coe_apply, Perfection.pthRootMonoidHom_eq_symm_frobeniusEquiv, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, DoubleQuot.quotQuotEquivQuotSup_quotQuotMk, RingEquiv.toSemiRingCatIso_hom, Ring.DirectLimit.ringEquiv_symm_mk, RingEquiv.coe_ringHom_refl, frobeniusEquiv_symm_pow_p, Padic.withValUniformEquiv_cast_apply, RingAut.coe_one, cyclotomicCharacter.toZModPow_toFun, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk, RingEquiv.map_sum, Padic.coe_withValRingEquiv, frobenius_apply_frobeniusEquiv_symm, UniformSpace.Completion.mapRingEquiv_apply, TruncatedWittVector.zmodEquivTrunc_apply, RingEquiv.ofRingHom_apply, IsSemisimpleRing.exists_ringEquiv_pi_matrix_end_mulOpposite, trace_quotient_eq_trace_localization_quotient, Ideal.quotientEquiv_mk, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, RingEquiv.coe_prodCongr, RingEquiv.toMulEquiv_eq_coe, LinearEquiv.conjRingEquiv_symm_apply_apply, RingEquiv.piCongrLeft'_symm_apply, RingEquiv.toSemilinearEquiv_apply, Perfection.lift_apply_apply_coe, RingEquiv.zeroRingProd_apply, LaurentSeries.tendsto_valuation, RingHom.ker_coe_equiv, RingHomInvPair.of_ringEquiv, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk, Perfection.pthRoot_eq_symm_frobeniusEquiv, PreTilt.untilt_iterate_frobeniusEquiv_symm_pow, RingEquiv.op_symm_apply_apply, RingEquiv.symm_toSemilinearEquiv_symm_apply, WithAbs.equiv_apply, MonoidAlgebra.toRingHom_mapRangeRingEquiv, modularCyclotomicCharacter.comp, ZMod.subsingleton_ringEquiv, NonUnitalSubsemiring.centerToMulOpposite_apply_coe, HahnSeries.coeff_toMvPowerSeries, RCLike.realRingEquiv_apply, MonoidAlgebra.mapDomainRingEquiv_apply, PerfectionMap.surjective, AlgebraicGeometry.Proj.stalkIso'_germ, cyclotomicCharacter.spec, Valuation.IsEquiv.uniformContinuous_equiv_symm, IsDedekindDomain.HeightOneSpectrum.adicValued_apply', Subsemiring.topEquiv_symm_apply_coe, RingEquiv.sumArrowEquivProdArrow_apply, IsSimpleRing.exists_ringEquiv_matrix_divisionRing, RingEquiv.image_eq_preimage_symm, WithVal.equivWithVal_apply, AlgEquiv.ofRingEquiv_toEquiv, AlgEquiv.opComm_symm_apply_symm_apply, IsDedekindDomain.HeightOneSpectrum.equivOfRingEquiv_apply, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, Padic.coe_withValRingEquiv_symm, RingEquiv.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, RingEquiv.toRingHom_eq_coe, RingEquiv.map_multiset_sum, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, IsLocalization.ringEquivOfRingEquiv_eq, FractionalIdeal.map_canonicalEquiv_mk0, Rat.ringOfIntegersEquiv_symm_apply_coe, RingEquiv.coe_ringHom_ofRingHom, Polynomial.opRingEquiv_symm_C, FractionalIdeal.mem_canonicalEquiv_apply, rootsOfUnity.integer_power_of_ringEquiv', RingEquiv.piFinTwo_symm_apply, Module.Basis.mapCoeffs_repr, WittVector.frobeniusEquiv_apply, RingEquiv.symm_comp, HahnSeries.ofPowerSeries_apply, RingHom.quotientKerEquivOfRightInverse.apply, RingEquiv.toRingHom_injective, 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, RingEquiv.map_eq_neg_one_iff, RingEquiv.unop_map_list_prod, RingEquiv.map_multiset_prod, RingEquiv.coe_addEquiv_trans, IsInertiaField.algebraMap_ringEquiv_apply, PerfectionMap.comp_symm_equiv', IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_apply_mk, DoubleQuot.quotQuotEquivComm_mk_mk, Matrix.conjTransposeRingEquiv_apply, Matrix.compRingEquiv_apply, RingEquiv.coe_addMonoidHom_trans, Language.reverseIso_symm_apply, RingEquiv.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, RingEquiv.coe_toAddEquiv_symm, Subsemiring.comap_equiv_eq_map_symm, DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk, RingEquiv.coe_trans, starRingEquiv_apply, NumberField.ComplexEmbedding.isReal_comp_iff, addMonoidAlgebraRingEquivDirectSum_apply, RingAut.mul_apply, Submodule.mulMap_op, RingEquiv.eq_symm_apply, addMonoidEndRingEquivInt_symm_apply, DoubleQuot.coe_quotQuotEquivCommₐ, addMonoidAlgebraRingEquivDirectSum_symm_apply, RingEquiv.image_symm_eq_preimage, RingEquiv.coe_toMulEquiv_symm, Ideal.fst_comp_quotientInfEquivQuotientProd, RingEquiv.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, RingEquiv.opOp_symm_apply, ClassGroup.mk_canonicalEquiv, ValuationRing.coe_equivInteger_apply, Subsemiring.mopRingEquivOp_symm_apply, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, RingHom.rangeRestrictFieldEquiv_apply_coe, RingEquiv.bijective, ModuleCat.endRingEquiv_apply, WittVector.ghostEquiv_coe, RatFunc.toFractionRingRingEquiv_apply, Algebra.norm_eq_of_ringEquiv, RingEquiv.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, UniformSpace.Completion.mapRingEquiv_symm_apply, ZMod.ringEquivCongr_val, LaurentSeries.mem_integers_of_powerSeries, Polynomial.mapEquiv_apply, PerfectRing.liftAux_apply, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion, coe_iterateFrobeniusEquiv, HahnSeries.toPowerSeries_apply, IsLocalRing.map_ringEquiv_maximalIdeal, Ideal.snd_comp_quotientInfEquivQuotientProd, RingEquiv.coe_monoidHom_refl, Algebra.trace_eq_of_equiv_equiv, MonoidHom.map_iterate_frobeniusEquiv_symm, ZMod.ringEquivCongr_intCast, RingEquiv.ofHomInv'_symm_apply, RingCon.quotientKerEquivOfSurjective_mk, RingEquiv.refl_apply, RingEquiv.nonUnitalSubsemiringMap_apply_coe, Module.End.ringEquivEndFinsupp_symm_apply_apply, RingEquiv.piOptionEquivProd_symm_apply, BitVec.equivFin_apply, Ideal.Factors.piQuotientEquiv_mk, Equiv.ringEquiv_symm_apply, RingEquiv.piFinTwo_apply, IsInertiaField.algebraMap_ringEquiv_symm_apply, PerfectionMap.lift_apply, NonUnitalSubring.centerToMulOpposite_apply_coe, RingEquiv.prodProdProdComm_toEquiv, Subring.ringEquivOpMop_apply, WithAbs.equiv_symm_apply, HahnSeries.toPowerSeries_symm_apply_coeff, RingEquiv.coe_toRingHom, AlgebraicGeometry.Proj.stalkIso'_symm_mk, RingEquiv.piUnique_apply, RingEquiv.fst_comp_coe_prodComm, WithVal.equivWithVal_symm_apply, StarRingEquiv.coe_mk, MonoidAlgebra.opRingEquiv_apply, RingEquiv.opOp_apply, RingEquiv.ofBijective_symm_comp, AbsoluteValue.isEquiv_iff_isHomeomorph, RingEquiv.prodProdProdComm_toAddEquiv, NumberField.RingOfIntegers.mapRingEquiv_symm_apply, IsDedekindDomain.quotientEquivPiFactors_mk, AdjoinRoot.coe_mapRingEquiv, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, MonoidAlgebra.commRingEquiv_single_single, AlgEquiv.ofRingEquiv_symm_apply, Real.ringEquivCauchy_symm_apply_cauchy, AbsoluteValue.Completion.extensionEmbedding_of_comp_coe, ClassGroup.mk_def, IsSeparable.of_equiv_equiv, minpoly.map_eq_of_equiv_equiv, modularCyclotomicCharacter.aux_spec, modularCyclotomicCharacter'.unique', IsSemisimpleModule.exists_end_ringEquiv_pi_matrix_end, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, LaurentSeries.uniformContinuous_withVal_equiv, Ideal.spanFinrank_map_eq_of_ringEquiv, PerfectionMap.equiv_apply, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk, map_prime_of_equiv, cyclotomicCharacter.continuous, IsGaloisGroup.algebraMap_ringEquiv_apply, Int.quotientSpanNatEquivZMod_comp_castRingHom, 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, RingEquiv.toSemiRingCatIso_inv, RingAut.coe_pow, DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk, OrderRingIso.coe_toRingEquiv, frobeniusEquiv_symm_apply_frobenius, RingEquiv.coe_mulEquiv_refl, Polynomial.roots_X_pow_char_pow_sub_C, AddMonoidAlgebra.mapRingEquiv_single, RingEquiv.prodCongr_symm_apply, CategoryTheory.Iso.commSemiRingCatIsoToRingEquiv_toRingHom, Ideal.Factors.piQuotientEquiv_map, RingEquiv.coe_refl, NonUnitalSubsemiring.topEquiv_symm_apply_coe, RingEquiv.moduleEndSelfOp_symm_apply, RingEquiv.comp_symm, NonUnitalSubsemiring.topEquiv_apply, DoubleQuot.quotQuotEquivComm_algebraMap, IsLocalization.ringEquivOfRingEquiv_mk', AlgEquiv.coe_ringHom_commutes, RingCon.comapQuotientEquivOfSurj_mk, Module.compHom.toLinearEquiv_apply, RingHomInvPair.of_ringEquiv_symm, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply
|