| Metric | Count |
|---|
Definitionsapply, symm_apply, toEquiv, algHomUnitsEquiv, applyMulSemiringAction, arrowCongr, aut, autCongr, cast, equivCongr, hasCoeToRingEquiv, instEquivLike, instFunLike, instInhabited, instMulDistribMulActionUnits, ofAlgHom, ofBijective, ofLinearEquiv, aux, ofRingEquiv, refl, aux, toAddEquiv, toAlgHom, toAlgHomHom, toEquiv, toLinearEquiv, toLinearMap, toLinearMapHom, toMulEquiv, toRingEquiv, trans, AlgEquivClass, instCoeTCAlgEquiv, toAlgEquiv, algConj, algEquivOfRing, conjAlgEquiv, toAlgAut, toAlgEquiv, algEquiv, instUniqueAlgEquivOfSubsingleton, «term_≃ₐ[_]_» | 43 |
TheoremsalgHomUnitsEquiv_apply_apply, algHomUnitsEquiv_apply_symm_apply, algebraMap_eq_apply, apply_faithfulSMul, apply_smulCommClass, apply_smulCommClass', apply_symm_apply, arrowCongr_apply, arrowCongr_comp, arrowCongr_refl, arrowCongr_symm, arrowCongr_trans, autCongr_apply, autCongr_refl, autCongr_symm, autCongr_trans, aut_inv, aut_mul, aut_one, bijective, cast_apply, cast_symm_apply, coe_algHom, coe_algHom_injective, coe_algHom_ofAlgHom, coe_apply_coe_coe_symm_apply, coe_coe, coe_coe_symm_apply_coe_apply, coe_fun_injective, coe_inv, coe_mk, coe_ofBijective, coe_pow, coe_refl, coe_ringEquiv, coe_ringEquiv', coe_ringEquiv_injective, coe_ringHom_commutes, coe_symm_toLinearEquiv, coe_toEquiv, coe_toLinearEquiv, coe_trans, commutes, commutes', comp_symm, congr_arg, congr_fun, default_apply, eq_symm_apply, equivCongr_apply, equivCongr_refl, equivCongr_symm, equivCongr_trans, ext, ext_iff, injective, instAlgEquivClass, invFun_eq_symm, leftInverse_symm, linearEquivConj_mulLeft, linearEquivConj_mulLeftRight, linearEquivConj_mulRight, map_add', map_mul', mk_coe, mk_coe', mul_apply, ofAlgHom_apply, ofAlgHom_coe_algHom, ofAlgHom_symm, ofAlgHom_symm_apply, ofBijective_apply, ofBijective_apply_symm_apply, ofBijective_symm_apply_apply, ofLinearEquiv_apply, ofLinearEquiv_symm, ofLinearEquiv_toLinearEquiv, ofRingEquiv_apply, ofRingEquiv_symm_apply, ofRingEquiv_toEquiv, one_apply, one_toLinearMap, pow_toLinearMap, refl_symm, refl_toAlgHom, refl_toRingHom, rightInverse_symm, self_trans_symm, smul_def, smul_units_def, surjective, symm_apply_apply, symm_apply_eq, symm_bijective, symm_comp, symm_mk, symm_symm, symm_toAddEquiv, symm_toEquiv_eq_symm, symm_toMulEquiv, symm_toRingEquiv, symm_trans_apply, symm_trans_self, toAlgHomHom_apply, toAlgHom_apply, toAlgHom_eq_coe, toAlgHom_ofBijective, toAlgHom_toLinearMap, toAlgHom_toRingHom, toEquiv_eq_coe, toLinearEquiv_apply, toLinearEquiv_injective, toLinearEquiv_ofLinearEquiv, toLinearEquiv_refl, toLinearEquiv_symm, toLinearEquiv_toLinearMap, toLinearEquiv_trans, toLinearMapHom_apply_apply, toLinearMap_apply, toLinearMap_injective, toLinearMap_ofAlgHom, toLinearMap_ofBijective, toRingEquiv_eq_coe, toRingEquiv_symm, toRingEquiv_toRingHom, toRingHom_trans, trans_apply, trans_toLinearMap, val_algHomUnitsEquiv_symm_apply, val_inv_algHomUnitsEquiv_symm_apply, commutes, toAlgHomClass, toLinearEquivClass, toRingEquivClass, algEquiv, algEquivOfRing_apply, algEquivOfRing_symm_apply, conjAlgEquiv_apply, conjAlgEquiv_apply_apply, conjAlgEquiv_symm_apply_apply, symm_conjAlgEquiv, toAlgAut_apply, toAlgEquiv_apply, toAlgEquiv_injective, toAlgEquiv_symm_apply, toAlgEquiv_toEquiv, toRingEquiv_algEquiv, algEquiv_apply | 148 |
| Total | 191 |
| Name | Category | Theorems |
|---|
algHomUnitsEquiv 📖 | CompOp | 4 mathmath: algHomUnitsEquiv_apply_symm_apply, val_algHomUnitsEquiv_symm_apply, val_inv_algHomUnitsEquiv_symm_apply, algHomUnitsEquiv_apply_apply
|
applyMulSemiringAction 📖 | CompOp | 13 mathmath: apply_smulCommClass', Normal.minpoly_eq_iff_mem_orbit, smul_def, IsGaloisGroup.of_isGalois, instSMulDistribClassAlgEquiv, Algebra.isInvariant_of_isGalois', stabilizer_isOpen_of_isIntegral, isConjRoot_iff_orbitRel, apply_faithfulSMul, MulSemiringAction.toRingEquiv_algEquiv, cyclotomicCharacter.continuous, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, apply_smulCommClass
|
arrowCongr 📖 | CompOp | 5 mathmath: arrowCongr_apply, arrowCongr_comp, arrowCongr_trans, arrowCongr_symm, arrowCongr_refl
|
aut 📖 | CompOp | 180 mathmath: Polynomial.Gal.galActionHom_restrict, InfiniteGalois.normal_iff_isGalois, galRestrict_symm_algebraMap_apply, Ideal.Quotient.map_ker_stabilizer_subtype, Ideal.exists_comap_galRestrict_eq, NumberField.IsCMField.zpowers_complexConj_eq_top, autAdjoinRootXPowSubCEquiv_root, one_apply, Algebra.isInvariant_of_isGalois, Polynomial.Gal.restrict_smul, NumberField.InfinitePlace.nat_card_stabilizer_eq_one_or_two, Ideal.coe_smul_primesOver_mk_eq_map_galRestrict, NumberField.InfinitePlace.isUnramified_iff_card_stabilizer_eq_one, InfiniteGalois.isOpen_and_normal_iff_finite_and_isGalois, IsFractionRing.fieldEquivOfAlgEquivHom_apply, InfiniteGalois.normalAutEquivQuotient_apply, NumberField.InfinitePlace.exists_smul_eq_of_comap_eq, apply_smulCommClass', IsGaloisGroup.mulEquivAlgEquiv_apply_symm_apply, Normal.minpoly_eq_iff_mem_orbit, IsGalois.card_fixingSubgroup_eq_finrank, autEquivZmod_symm_apply_natCast, coe_inv, FiniteGaloisIntermediateField.mem_fixingSubgroup_iff, NumberField.InfinitePlace.IsUnramified.stabilizer_eq_bot, autAdjoinRootXPowSubCEquiv_symm_smul, NumberField.InfinitePlace.card_stabilizer, restrictNormalHom_surjective, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, NumberField.InfinitePlace.smul_apply, FiniteField.orderOf_frobeniusAlgEquivOfAlgebraic, pow_toLinearMap, InfiniteGalois.krullTopology_mem_nhds_one_iff_of_isGalois, NumberField.ComplexEmbedding.IsConj.coe_stabilizer_mk, IsCyclotomicExtension.isMulCommutative, aut_inv, Ideal.Quotient.stabilizerHom_surjective, aut_one, Polynomial.Gal.restrictDvd_def, InfiniteGalois.fixingSubgroup_fixedField, Algebra.IsQuadraticExtension.isMulCommutative_galoisGroup, isCyclic_of_isSplittingField_X_pow_sub_C, NumberField.IsCMField.orderOf_complexConj, IntermediateField.fixingSubgroup_top, NumberField.InfinitePlace.smul_eq_comap, coe_galRestrict_apply, NumberField.InfinitePlace.smul_mk, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, IsPrimitiveRoot.coe_autToPow_apply, IntermediateField.restrictRestrictAlgEquivMapHom_apply, IsGalois.intermediateFieldEquivSubgroup_apply, coe_pow, IntermediateField.map_fixingSubgroup, top_fixedByFinite, algebraMap_galRestrict_apply, IntermediateField.restrictRestrictAlgEquivMapHom_surjective, NumberField.InfinitePlace.isUnramified_smul_iff, NumberField.InfinitePlace.orbitRelEquiv_apply_mk'', IsAbelianGalois.toIsMulCommutative, smul_def, IsScalarTower.AlgEquiv.restrictNormalHom_comp, IsPrimitiveRoot.autToPow_injective, IntermediateField.fixedField_antitone, InfiniteGalois.mulEquivToLimit_symm_continuous, InfiniteGalois.isOpen_mulEquivToLimit_image_fixingSubgroup, IsGaloisGroup.of_isGalois, Ideal.Quotient.stabilizerHom_surjective_of_profinite, NumberField.InfinitePlace.smul_coe_apply, autEquivZmod_symm_apply_intCast, IsGalois.normalAutEquivQuotient_apply, IsGalois.normalBasis_apply, instSMulDistribClassAlgEquiv, IntermediateField.finrank_eq_fixingSubgroup_index, IsGaloisGroup.mulEquivAlgEquiv_apply_apply, IsFractionRing.stabilizerHom_surjective, InfiniteGalois.proj_adjoin_singleton_val, NumberField.InfinitePlace.isComplex_smul_iff, Ideal.Quotient.stabilizerHom_apply, groupCohomology.norm_ofAlgebraAutOnUnits_eq, IntermediateField.fixingSubgroup_le, IntermediateField.restrictRestrictAlgEquivMapHom_injective, IsGalois.intermediateFieldEquivSubgroup_symm_apply_toDual, Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, toLinearMapHom_apply_apply, IntermediateField.fixingSubgroup_antitone, InfiniteGalois.restrict_fixedField, autCongr_symm, autCongr_refl, NumberField.InfinitePlace.isUnramified_mk_iff_forall_isConj, IntermediateField.fixingSubgroup_isClosed, NumberField.InfinitePlace.isRamified_iff_card_stabilizer_eq_two, IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, isSolvable_of_isScalarTower, algHomUnitsEquiv_apply_symm_apply, Algebra.isInvariant_of_isGalois', instIsTopologicalGroupAlgEquiv, val_algHomUnitsEquiv_symm_apply, IsGalois.intermediateFieldEquivSubgroup_symm_apply, FixedPoints.toAlgAut_surjective, NumberField.InfinitePlace.isReal_smul_iff, IsGalois.fixedField_top, stabilizer_isOpen_of_isIntegral, InfiniteGalois.isOpen_iff_finite, one_toLinearMap, IntermediateField.map_fixingSubgroup_index, autCongr_apply, restrictNormalHom_id, galRestrict_apply, IntermediateField.finrank_fixedField_eq_card, InfiniteGalois.toAlgEquivAux_eq_liftNormal, mul_apply, NumberField.InfinitePlace.comap_smul, NumberField.InfinitePlace.not_isUnramified_iff_card_stabilizer_eq_two, Ideal.coe_smul_primesOver_eq_map_galRestrict, IsFractionRing.fieldEquivOfAlgEquivHom_injective, Ideal.Quotient.ker_stabilizerHom, Algebra.IsQuadraticExtension.isCyclic, Polynomial.Gal.restrict_surjective, NumberField.InfinitePlace.isUnramified_iff_stabilizer_eq_bot, val_inv_algHomUnitsEquiv_symm_apply, FiniteField.instIsCyclicAlgEquivOfFinite, isConjRoot_iff_orbitRel, InfiniteGalois.finGaloisGroupFunctor_map_proj_eq_proj, Algebra.IsAlgebraic.algEquivEquivAlgHom_apply, InfiniteGalois.restrictNormalHom_continuous, krullTopology_mem_nhds_one_iff, smul_units_def, MulSemiringAction.toAlgAut_apply, krullTopology_mem_nhds_one_iff_of_normal, Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply, IsGalois.map_fixingSubgroup, IntermediateField.fixingSubgroup_isOpen, NumberField.InfinitePlace.mem_stabilizer_mk_iff, mem_galBasis_iff, IsGaloisGroup.mulEquivAlgEquiv_symm_apply, restrictNormalHom_apply, InfiniteGalois.mk_toAlgEquivAux, FiniteField.bijective_frobeniusAlgEquivOfAlgebraic_pow, IntermediateField.le_iff_le, InfiniteGalois.fixedField_bot, apply_faithfulSMul, IsPrimitiveRoot.autToPow_spec, InfiniteGalois.proj_of_le, Polynomial.Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, FiniteField.Extension.exists_frob_pow_eq, NumberField.InfinitePlace.mem_orbit_iff, autEquivRootsOfUnity_apply_rootOfSplit, IntermediateField.fixedField_bot, FixedPoints.toAlgAut_bijective, IsGalois.fixingSubgroup_normal_of_isGalois, InfiniteGalois.algEquivToLimit_continuous, IsScalarTower.AlgEquiv.restrictNormalHom_comp_apply, IntermediateField.restrictNormalHom_ker, NumberField.ComplexEmbedding.IsConj.comp, IsGalois.tfae, toAlgHomHom_apply, aut_mul, NumberField.ComplexEmbedding.IsReal.isConjGal_one, MulSemiringAction.toRingEquiv_algEquiv, autAdjoinRootXPowSubC_root, NumberField.ComplexEmbedding.isConj_one_iff, IntermediateField.fixingSubgroup_bot, IntermediateField.mem_fixingSubgroup_iff, NumberField.ComplexEmbedding.IsConj.isUnramified_mk_iff, InfiniteGalois.fixingSubgroup_isClosed, IntermediateField.fixingSubgroup_sup, NumberField.ComplexEmbedding.orderOf_isConj_two_of_ne_one, cyclotomicCharacter.continuous, IsGaloisGroup.map_mulEquivAlgEquiv_fixingSubgroup, IsCyclotomicExtension.autEquivPow_symm_apply, algHomUnitsEquiv_apply_apply, autCongr_trans, IsCyclotomicExtension.autEquivPow_apply, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, isCyclic_tfae, IsGalois.ofDual_intermediateFieldEquivSubgroup_apply, apply_smulCommClass, prod_galRestrict_eq_norm, autEquivRootsOfUnity_smul
|
autCongr 📖 | CompOp | 4 mathmath: autCongr_symm, autCongr_refl, autCongr_apply, autCongr_trans
|
cast 📖 | CompOp | 2 mathmath: cast_symm_apply, cast_apply
|
equivCongr 📖 | CompOp | 4 mathmath: equivCongr_symm, equivCongr_apply, equivCongr_refl, equivCongr_trans
|
hasCoeToRingEquiv 📖 | CompOp | — |
instEquivLike 📖 | CompOp | 129 mathmath: Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ, Subalgebra.mulMap_comm, coe_restrictScalars_symm, toAlgHom_toRingHom, refl_toRingHom, FractionalIdeal.mapEquiv_apply, Ideal.exists_comap_galRestrict_eq, MvPolynomial.comapEquiv_symm_coe, Polynomial.toAlgHom_taylorEquiv, Ideal.ramificationIdx_comap_eq, Complex.real_algHom_eq_id_or_conj, FractionalIdeal.map_one_div, Algebra.TensorProduct.congr_symm_apply, toRingEquiv_toRingHom, Ideal.inertiaDeg_comap_eq, PowerBasis.quotientEquivQuotientMinpolyMap_apply, MvPolynomial.comapEquiv_coe, AlgebraicGeometry.localRingHom_comp_stalkIso_apply, DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv, integralClosure_map_algEquiv, Ideal.quotientEquivAlgOfEq_coe_eq_factor, symm_toEquiv_eq_symm, adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, prodCongr_apply, toAlgHom_eq_coe, LocallyConstant.congrRightₐ_apply_apply, NumberField.InfinitePlace.smul_eq_comap, coe_galRestrict_apply, NumberField.InfinitePlace.smul_mk, LocallyConstant.congrRightₐ_symm_apply_apply, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, Polynomial.toMvPolynomial_eq_rename_comp, IsPrimitiveRoot.coe_autToPow_apply, Polynomial.comap_taylorEquiv_degreeLT, op_apply_symm_apply, symm_toMulEquiv, coe_ringEquiv_injective, IsSymmetricAlgebra.equiv_symm_comp, Complex.liftAux_neg_I, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, AlgHom.ker_coe_equiv, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ, toAlgHom_toLinearMap, galLiftEquiv_apply, IsLocalization.algEquiv_comp_algebraMap_apply, Algebra.TensorProduct.leftComm_toLinearEquiv, Algebra.TensorProduct.congr_apply, NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq, symm_toAddEquiv, IntermediateField.normal_iff_forall_map_le', MulSemiringAction.toAlgEquiv_toEquiv, symm_comp, galLiftEquiv_symm_apply, coe_ringEquiv, toRingEquiv_opOp, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, toAlgHom_ofBijective, op_symm_apply_symm_apply, FractionalIdeal.coeFun_mapEquiv, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, IsAzumaya.coe_tensorEquivEnd, coe_algHom_injective, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, NumberField.RingOfIntegers.withValEquiv_apply, coe_restrictScalars, Algebra.TensorProduct.comm_comp_includeRight, Algebra.TensorProduct.comm_comp_includeLeft, IsAdicComplete.ofAlgEquiv_comp_liftRingHom, BialgEquiv.toAlgEquiv_toRingHom, refl_toAlgHom, FractionalIdeal.map_div, FractionalIdeal.map_inv, Polynomial.mapAlgEquiv_toAlgHom, MvPolynomial.finSuccEquiv_comp_C_eq_C, MvPolynomial.finSuccEquiv_eq, instAlgEquivClass, opComm_apply_symm_apply, subalgebraMap_apply_coe, IsLocalization.algEquiv_comp_algebraMap, toRingHom_trans, galRestrict_apply, coe_toEquiv, IntermediateField.normalClosure_def'', NumberField.InfinitePlace.comap_smul, IntermediateField.normal_iff_forall_map_eq', Localization.coe_algEquiv, ofLinearEquiv_symm, minpoly.equivAdjoin_toAlgHom, DoubleQuot.quotQuotEquivCommₐ_toRingEquiv, DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv, toEquiv_eq_coe, fieldRange_eq_top, smul_units_def, comp_symm, Polynomial.aeval_algEquiv, IsGalois.map_fixingSubgroup, ofRingEquiv_toEquiv, opComm_symm_apply_symm_apply, DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv, Polynomial.mapAlgEquiv_coe_ringHom, toRingEquiv_toOpposite, coe_algHom_ofAlgHom, Algebra.TensorProduct.comm_comp_map, FractionalIdeal.map_map_symm, DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ, IsAdjoinRoot.algEquiv_map, algebraicClosure.map_eq_of_algEquiv, NumberField.ComplexEmbedding.IsConj.comp, FractionalIdeal.map_symm_map, StandardEtalePresentation.toPresentation_relation, symm_toRingEquiv, separableClosure.map_eq_of_algEquiv, MulSemiringAction.toRingEquiv_algEquiv, subalgebraMap_symm_apply_coe, IsSymmetricAlgebra.equiv_toAlgHom, prodCongr_symm_apply, Polynomial.coe_taylorEquiv, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, toRingEquiv_symm, Polynomial.taylorLinearEquiv_apply_coe, Rat.ringOfIntegersWithValEquiv_apply, Ideal.relNorm_comap_algEquiv, extendScalarsOfSurjective_apply, NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq, Polynomial.map_taylorEquiv_degreeLT, Polynomial.coe_mapAlgEquiv, Localization.coe_algEquiv_symm, coe_ringHom_commutes, toRingEquiv_eq_coe
|
instFunLike 📖 | CompOp | 812 mathmath: FiniteField.Extension.frob_apply, MvPolynomial.pUnitAlgEquiv_symm_monomial, Algebra.PreSubmersivePresentation.jacobian_ofAlgEquiv, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ, Polynomial.Gal.galActionHom_restrict, AdjoinRoot.algEquivOfAssociated_apply_root, Subalgebra.mulMap_comm, Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply, Matrix.toLinAlgEquiv_one, SkewMonoidAlgebra.domCongr_support, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, moduleEndSelfOp_apply_apply, toAlgHom_toRingHom, LinearMap.toMatrixAlgEquiv'_mul, leftInverse_symm, MvPolynomial.pUnitAlgEquiv_apply, refl_toRingHom, FractionalIdeal.mapEquiv_apply, Polynomial.algEquivCMulXAddC_apply, coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, galRestrict_symm_algebraMap_apply, opOp_apply, Algebra.TensorProduct.prodRight_tmul_fst, IsLocalization.algEquiv_symm_mk', Quaternion.snd_imJ_dualNumberEquiv_symm, Ideal.exists_comap_galRestrict_eq, MvPolynomial.support_finSuccEquiv, MvPolynomial.rTensorAlgEquiv_apply, MvPolynomial.mem_image_support_coeff_finSuccEquiv, MvPolynomial.comapEquiv_symm_coe, IntermediateField.coe_algebraMap_over_bot, Polynomial.toAlgHom_taylorEquiv, autAdjoinRootXPowSubCEquiv_root, one_apply, Ideal.ramificationIdx_comap_eq, Matrix.compAlgEquiv_apply, minpoly.algEquiv_apply, Complex.real_algHom_eq_id_or_conj, FractionalIdeal.map_one_div, Submodule.coe_mapAlgEquiv_symm_apply, Polynomial.Gal.restrict_smul, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm, IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen, Algebra.IsPushout.equiv_symm_algebraMap_left, DirectSum.decomposeAlgEquiv_symm_apply, Ideal.coe_smul_primesOver_mk_eq_map_galRestrict, AdicCompletion.of_ofAlgEquiv_symm, Polynomial.fiberEquivQuotient_tmul, LinearEquiv.algEquivOfRing_apply, MvPolynomial.optionEquivLeft_C, toOpposite_apply, LinearMap.toMatrixAlgEquiv_comp, Algebra.TensorProduct.congr_symm_apply, isTranscendenceBasis_iff, MvPolynomial.optionEquivLeft_X_some, toRingEquiv_toRingHom, Subalgebra.equivOfEq_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, MvPolynomial.pUnitAlgEquiv_symm_apply, Polynomial.quotientSpanXSubCAlgEquiv_symm_apply, LinearEquiv.conjAlgEquiv_symm_apply_apply, toOpposite_symm_apply, isConjRoot_of_algEquiv, coe_ringEquiv', CliffordAlgebraDualNumber.equiv_symm_eps, minpoly.exists_algEquiv_of_root', Ideal.inertiaDeg_comap_eq, IsAdjoinRoot.algEquiv_algEquiv, MvPolynomial.natDegree_finSuccEquiv, StandardEtalePresentation.toPresentation_algebra_smul, IsSymmetricAlgebra.equiv_apply, FiniteField.frobeniusAlgEquivOfAlgebraic_apply, IsLocalization.algEquiv_apply, linearEquivConj_mulLeft, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk, Algebra.TensorProduct.prodRight_symm_tmul, Localization.algEquiv_apply, IsGaloisGroup.mulEquivAlgEquiv_apply_symm_apply, isConjRoot_iff_exists_algEquiv, Localization.algEquiv_mk', PowerBasis.quotientEquivQuotientMinpolyMap_apply, MvPolynomial.comapEquiv_coe, IntermediateField.botEquiv_symm, Polynomial.pUnitAlgEquiv_symm_toPowerSeries, op_apply_apply, adjoinRootXPowSubCEquiv_symm_eq_root, ofInjective_apply, ULift.algEquiv_apply, Quaternion.snd_re_dualNumberEquiv_symm, Ideal.Quotient.algEquivOfEqMap_apply, MvPolynomial.optionEquivLeft_apply, MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le, LinearMap.toMatrixAlgEquiv_toLinAlgEquiv, autEquivZmod_symm_apply_natCast, coe_inv, InfiniteGalois.mem_bot_iff_fixed, symm_apply_eq, CliffordAlgebra.equivBaseChange_symm_apply, prodQuotientOfIsIdempotentElem_apply, matPolyEquiv_map_smul, Quaternion.imJ_fst_dualNumberEquiv, StarAlgEquiv.coe_toAlgEquiv, MvPolynomial.supportedEquivMvPolynomial_symm_X, SkewMonoidAlgebra.domCongrAlg_apply, integralClosure_map_algEquiv, autAdjoinRootXPowSubCEquiv_symm_smul, matPolyEquiv_diagonal_X, Algebra.TensorProduct.piScalarRight_tmul, isSeparable_iff, IsGalois.mem_range_algebraMap_iff_fixed, AdjoinRoot.algEquivOfAssociated_root, Algebra.TensorProduct.comm_comp_map_apply, RingCon.coe_comapQuotientEquivRangeₐ_mk, Algebra.trace_eq_of_algEquiv, PowerBasis.equivAdjoinSimple_symm_aeval, MvPolynomial.optionEquivRight_C, InfiniteGalois.toAlgEquivAux_eq_proj_of_mem, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, NumberField.InfinitePlace.smul_apply, Algebra.TensorProduct.assoc_tmul, MvPolynomial.degreeOf_coeff_finSuccEquiv, NumberField.RingOfIntegers.withValEquiv_symm_apply, coe_refl, Quaternion.imI_fst_dualNumberEquiv, FiniteField.coe_frobeniusAlgEquivOfAlgebraic, LinearMap.toMatrixAlgEquiv'_id, LinearEquiv.conjAlgEquiv_apply, Ideal.quotientEquivAlgOfEq_coe_eq_factor, MvPolynomial.nonempty_support_finSuccEquiv, Algebra.TensorProduct.algEquivIncludeRange_symm_tmul, adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, Algebra.TensorProduct.leftComm_tmul, prodCongr_apply, Polynomial.Bivariate.aveal_eq_map_swap, quotientBot_mk, ofBijective_symm_apply_apply, toAlgHom_eq_coe, isConjRoot_of_algEquiv₂, Polynomial.Bivariate.swap_apply, LinearMap.toMatrixAlgEquiv_apply, LocallyConstant.congrRightₐ_apply_apply, isTranscendenceBasis, Algebra.Presentation.quotientEquiv_symm, MvPolynomial.eval₂_const_pUnitAlgEquiv_symm, MvPolynomial.support_finSuccEquiv_nonempty, Matrix.toLinAlgEquiv_mul, MvPolynomial.degree_optionEquivLeft, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, Algebra.TensorProduct.lid_tmul, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, NumberField.InfinitePlace.smul_eq_comap, Algebra.TensorProduct.tensorTensorTensorComm_symm_tmul, coe_galRestrict_apply, NumberField.InfinitePlace.smul_mk, matPolyEquiv_coeff_apply_aux_1, LocallyConstant.congrRightₐ_symm_apply_apply, default_apply, MvPolynomial.optionEquivRight_X_none, Subalgebra.mopAlgEquivOp_symm_apply, spectralNorm_eq_iSup_of_finiteDimensional_normal, Equiv.algEquiv_apply, TensorAlgebra.equivFreeAlgebra_symm_ι, LinearMap.detAux_def, ext_iff, matPolyEquiv_symm_apply_coeff, CommAlgCat.algEquivOfIso_apply, PiTensorProduct.constantBaseRingEquiv_symm, LinearMap.toMatrixAlgEquiv_id, Polynomial.toMvPolynomial_eq_rename_comp, Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_symm_apply, IsPrimitiveRoot.coe_autToPow_apply, IntermediateField.restrictRestrictAlgEquivMapHom_apply, Module.Invertible.algEquivOfRing_apply, PowerBasis.map_gen, Quaternion.fst_imK_dualNumberEquiv_symm, CommAlgCat.isoMk_hom, QuaternionAlgebra.imK_swapEquiv_symm_apply, LocallyConstant.congrLeftₐ_apply_apply, NumberField.ComplexEmbedding.IsConj.eq, coe_pow, MonoidAlgebra.domCongr_single, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, CategoryTheory.Iso.toAlgEquiv_symm_apply, MonoidAlgebra.scalarTensorEquiv_tmul, MvPolynomial.eval_eq_eval_mv_eval', PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, sumArrowEquivProdArrow_symm_apply_inr, CommAlgCat.algEquivOfIso_symm_apply, MvPolynomial.optionEquivLeft_X_none, MvPolynomial.optionEquivRight_symm_apply, PiTensorProduct.constantBaseRingEquiv_tprod, minpoly.exists_algEquiv_of_root, op_apply_symm_apply, commutes, mopMatrix_apply, Subalgebra.lTensorBot_one_tmul, TensorAlgebra.equivDirectSum_apply, algebraMap_galRestrict_apply, Matrix.det_reindexAlgEquiv, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, GradedTensorProduct.auxEquiv_comm, AddMonoidAlgebra.commAlgEquiv_single_single, TensorAlgebra.equivFreeAlgebra_ι_apply, MvPolynomial.finSuccEquiv_coeff_coeff, smul_def, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', Localization.algEquiv_mk, MvPolynomial.commAlgEquiv_C, MulSemiringAction.toAlgEquiv_symm_apply, IntermediateField.mem_fixedField_iff, NumberField.IsCMField.complexConj_apply_apply, MvPolynomial.commAlgEquiv_X, Algebra.TensorProduct.algEquivOfLinearEquivTensorProduct_apply, MvPolynomial.optionEquivRight_X_some, Matrix.TransvectionStruct.toMatrix_reindexEquiv_prod, Algebra.TensorProduct.opAlgEquiv_apply, eq_symm_apply, AddMonoidAlgebra.domCongr_single, Quaternion.imK_fst_dualNumberEquiv, NumberField.IsCMField.coe_ringOfIntegersComplexConj, minpoly.algEquiv_eq, Matrix.kroneckerAlgEquiv_apply, ofAlgHom_symm_apply, IsAdjoinRoot.adjoinRootAlgEquiv_apply_root, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, PowerBasis.equivOfMinpoly_gen, FiniteField.frobeniusAlgEquiv_symm_apply, CliffordAlgebraQuaternion.equiv_apply, Quaternion.re_fst_dualNumberEquiv, Complex.liftAux_neg_I, PowerBasis.equivAdjoinSimple_aeval, polyEquivTensor_symm_apply_tmul, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, AdjoinRoot.quotEquivQuotMap_apply, MvPolynomial.mapAlgEquiv_apply, Polynomial.Bivariate.equivMvPolynomial_symm_X_0, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, AddMonoidAlgebra.mapRangeAlgEquiv_apply, cast_symm_apply, Matrix.TransvectionStruct.toMatrix_reindexEquiv, BialgEquiv.coe_toAlgEquiv, MvPolynomial.tensorEquivSum_one_tmul_C, NumberField.InfinitePlace.smul_coe_apply, Ideal.quotientKerAlgEquivOfRightInverse_symm_apply, CliffordAlgebraQuaternion.equiv_symm_apply, AlgHom.ker_coe_equiv, Algebra.TensorProduct.commRight_tmul, Algebra.discr_eq_discr_of_algEquiv, autEquivZmod_symm_apply_intCast, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ, toAlgHom_toLinearMap, Subalgebra.topEquiv_apply, IsGalois.normalBasis_apply, NumberField.IsCMField.complexConj_apply_eq_self, opComm_apply_apply, MonoidAlgebra.tensorEquiv_symm_single, LinearMap.toMatrixAlgEquiv'_apply, galLiftEquiv_apply, MvPolynomial.optionEquivLeft_coeff_coeff, Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, Ideal.quotientKerAlgEquivOfRightInverse_apply, IsLocalization.algEquiv_comp_algebraMap_apply, IsPrimitiveRoot.associated_sub_one_map_sub_one, isConjRoot_of_algEquiv', ofLeftInverse_apply, MvPolynomial.renameEquiv_apply, addMonoidAlgebraAlgEquivDirectSum_symm_apply, Polynomial.quotientSpanXSubCAlgEquiv_mk, Matrix.uniqueAlgEquiv_apply, restrictScalars_symm_apply, AdicCompletion.mk_ofAlgEquiv_symm, IsGaloisGroup.mulEquivAlgEquiv_apply_apply, InfiniteGalois.proj_adjoin_singleton_val, Polynomial.Bivariate.swap_Y, IsPrimitiveRoot.associated_map_sub_one_map_sub_one, DoubleQuot.coe_quotQuotEquivQuotSupₐ, Subalgebra.coe_equivMapOfInjective_apply, IsFractionRing.fieldEquivOfAlgEquiv_algebraMap, NumberField.IsCMField.complexEmbedding_complexConj, apply_symm_apply, MonoidAlgebra.mapRangeAlgEquiv_apply, PowerBasis.equivAdjoinSimple_gen, ofBijective_apply, coe_symm_toLinearEquiv, FiniteField.frobeniusAlgEquivOfAlgebraic_symm_apply, Ideal.Quotient.stabilizerHom_apply, coe_apply_coe_coe_symm_apply, Algebra.TensorProduct.congr_apply, Polynomial.Bivariate.equivMvPolynomial_symm_C, Matrix.reindexAlgEquiv_mul, coe_mapIntegralClosure, IsIntegralClosure.algebraMap_equiv, coe_polyEquivTensor'_symm, PowerBasis.equivAdjoinSimple_symm_gen, funUnique_apply, MonoidAlgebra.commAlgEquiv_single_single, MvPolynomial.algebraTensorAlgEquiv_symm_X, MvPolynomial.support_coeff_finSuccEquiv, Matrix.kroneckerTMulAlgEquiv_symm_apply, coe_polyEquivTensor', Ideal.Quotient.exists_algEquiv_fixedPoint_quotient_under, toUnder_inv_right_apply, Submodule.coe_mapAlgEquiv_apply, StandardEtalePresentation.equivRing_x, piCongrLeft'_apply, NumberField.InfinitePlace.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq, piCongrLeft_apply, Complex.conjAe_coe, ofRingEquiv_apply, symm_trans_apply, QuaternionAlgebra.re_swapEquiv_symm_apply, Quaternion.fst_imJ_dualNumberEquiv_symm, FiniteField.coe_frobeniusAlgEquivOfAlgebraic_iterate, NonUnitalSubalgebra.unitizationAlgEquiv_apply_coe, PiTensorProduct.dualDistribEquivOfBasis_apply_apply, Polynomial.Bivariate.swap_X, groupCohomology.exists_div_of_norm_eq_one, toLieEquiv_symm_apply, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_apply, IntermediateField.normal_iff_forall_map_le', ofLinearEquiv_apply, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, CategoryTheory.Iso.toAlgEquiv_apply, ContinuousAlgEquiv.coe_toAlgEquiv, Polynomial.algEquivAevalNegX_symm_apply, Shrink.algEquiv_apply, symm_comp, Localization.algEquiv_symm_mk', IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map, RingCon.congrₐ_mk, cast_apply, toLinearMapHom_apply_apply, Matrix.dualNumberEquiv_symm_apply, Polynomial.Bivariate.equivMvPolynomial_symm_X_1, Matrix.matPolyEquiv_charmatrix, Algebra.TensorProduct.rid_tmul, galLiftEquiv_symm_apply, coe_ringEquiv, AdicCompletion.ofAlgEquiv_apply, IsConjRoot.exists_algEquiv, Algebra.pushoutDesc_apply, Algebra.TensorProduct.cancelBaseChange_tmul, isIntegral_algEquiv, Quaternion.fst_imI_dualNumberEquiv_symm, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, Polynomial.algEquivOfCompEqX_symm_apply, IsSymmetricAlgebra.equiv_symm_apply, toAlgHom_ofBijective, InfiniteGalois.limitToAlgEquiv_apply, MvPolynomial.mem_support_coeff_optionEquivLeft, HahnSeries.toPowerSeriesAlg_apply, groupCohomology.exists_mul_galRestrict_of_norm_eq_one, Polynomial.Bivariate.swap_C_C, Matrix.toLinAlgEquiv'_apply, HahnSeries.toPowerSeriesAlg_symm_apply_coeff, Localization.algEquiv_symm_mk, Polynomial.algEquivAevalXAddC_symm_apply, Ideal.Quotient.algEquivOfEqComap_apply, AdjoinRoot.algEquivOfEq_root, MvPolynomial.universalFactorizationMapPresentation_relation, IntermediateField.adjoinRootEquivAdjoin_apply_root, Ideal.quotientKerAlgEquivOfSurjective_apply, op_symm_apply_symm_apply, FractionalIdeal.coeFun_mapEquiv, AlgebraicIndependent.algebraMap_aevalEquiv, LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv', coe_restrictScalars', PowerBasis.equivOfMinpoly_aeval, Subalgebra.rTensorBot_tmul_one, LocallyConstant.congrLeftₐ_symm_apply_apply, Polynomial.Bivariate.swap_monomial_monomial, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, IsAzumaya.coe_tensorEquivEnd, AlgHom.tensorEqualizerEquiv_apply, coe_algHom_injective, MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le, NumberField.ComplexEmbedding.isConj_apply_apply, AdjoinRoot.quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, Polynomial.Bivariate.swap_map_C, MonoidAlgebra.tensorEquiv_tmul, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, Algebra.norm_eq_prod_automorphisms, QuaternionAlgebra.coe_starAe, QuaternionAlgebra.imI_swapEquiv_symm_apply, SymmetricAlgebra.equivMvPolynomial_symm_X, Algebra.TensorProduct.comm_comp_includeRight, CliffordAlgebraComplex.equiv_symm_apply, IsUltrametricDist.algNormOfAlgEquiv_apply, matrixEquivTensor_apply_single, restrictScalars_apply, RingCon.quotientQuotientEquivQuotientₐ_mk_mk, Algebra.TensorProduct.cancelBaseChange_symm_tmul, matPolyEquiv_map_C, IsLocalization.algEquiv_mk', Ideal.quotientEquivAlgOfEq_mk, Algebra.TensorProduct.comm_comp_includeLeft, NormedRing.algEquivComplexOfComplete_symm_apply, algHomUnitsEquiv_apply_symm_apply, IsAdicComplete.ofAlgEquiv_comp_liftRingHom, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, coe_coe_symm_apply_coe_apply, BialgEquiv.toAlgEquiv_toRingHom, coe_ofBijective, val_algHomUnitsEquiv_symm_apply, MvPolynomial.totalDegree_renameEquiv, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.isEmptyAlgEquiv_apply, refl_toAlgHom, Polynomial.Bivariate.equivMvPolynomial_X, Module.Basis.symmetricAlgebra_repr_apply, RingCon.coe_comapQuotientEquivRangeₐ_symm_mk, Algebra.TensorProduct.assoc_symm_tmul, Algebra.TensorProduct.opAlgEquiv_symm_apply, matrixEquivTensor_apply_symm, symm_apply_apply, MvPolynomial.natDegree_optionEquivLeft, FractionalIdeal.map_div, StarAlgEquiv.coe_symm_toAlgEquiv, Algebra.TensorProduct.algEquivIncludeRange_tmul, linearEquivConj_mulLeftRight, MvPolynomial.mem_support_finSuccEquiv, Quaternion.imJ_snd_dualNumberEquiv, FractionalIdeal.map_inv, coe_toLinearEquiv, LinearEquiv.conjAlgEquiv_apply_apply, Polynomial.mapAlgEquiv_toAlgHom, LinearEquiv.algEquivOfRing_symm_apply, eval_det, toAlgebraIso_inv, WithLp.unitizationAlgEquiv_symm_apply_ofLp, BialgEquiv.coe_toCoalgEquiv, toUnder_hom_right_apply, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, Subalgebra.lTensorBot_symm_apply, MvPolynomial.finSuccEquiv_comp_C_eq_C, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ, endVecAlgEquivMatrixEnd_apply_apply, Quaternion.snd_imK_dualNumberEquiv_symm, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk, Bialgebra.TensorProduct.coalgebra_rid_eq_algebra_rid_apply, RingCon.comapQuotientEquivRangeₐ_mk, MvPolynomial.finSuccEquiv_eq, SymmetricAlgebra.equivMvPolynomial_ι_apply, coe_algHom, MvPolynomial.ker_eval₂Hom_universalFactorizationMap, InfiniteGalois.mem_range_algebraMap_iff_fixed, MvPolynomial.image_support_finSuccEquiv, Polynomial.Bivariate.aevalAeval_swap, Subalgebra.algEquivOpMop_apply, Algebra.IsPushout.equiv_tmul, AddMonoidAlgebra.tensorEquiv_tmul, matPolyEquiv_symm_C, opComm_apply_symm_apply, Polynomial.Bivariate.equivMvPolynomial_C_X, NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff, PowerBasis.equivOfMinpoly_apply, Matrix.compAlgEquiv_symm_apply, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_root, CliffordAlgebra.prodEquiv_symm_apply, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, MvPolynomial.degree_finSuccEquiv, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.nonempty_support_optionEquivLeft, subalgebraMap_apply_coe, HahnSeries.ofPowerSeriesAlg_apply_coeff, RingCon.quotientQuotientEquivQuotientₐ_symm_mk, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, AdjoinRoot.algEquivOfEq_apply_root, Matrix.toLpLinAlgEquiv_apply_apply_ofLp, AddMonoidAlgebra.tensorEquiv_symm_single, adjoinRootXPowSubCEquiv_root, AdjoinRoot.equiv'_symm_apply, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, IsLocalization.algEquiv_comp_algebraMap, IsFractionRing.algEquivOfAlgEquiv_algebraMap, toRingHom_trans, NormedRing.algEquivComplexOfComplete_apply, Matrix.toLinAlgEquiv_apply, DirectSum.decomposeAlgEquiv_apply, Algebra.TensorProduct.comm_symm_tmul, CliffordAlgebra.prodEquiv_apply, MvPolynomial.support_optionEquivLeft, Algebra.norm_eq_of_algEquiv, MvPolynomial.finSuccEquiv_X_succ, MonoidAlgebra.scalarTensorEquiv_symm_single, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul, galRestrict_apply, Polynomial.toFinsuppIsoAlg_symm_apply_toFinsupp, CliffordAlgebra.involuteEquiv_apply, coe_toEquiv, CliffordAlgebra.evenEquivEvenNeg_apply, AddMonoidAlgebra.domCongr_support, MvPolynomial.eval₂_const_pUnitAlgEquiv, InfiniteGalois.toAlgEquivAux_eq_liftNormal, IntermediateField.normalClosure_def'', CliffordAlgebraComplex.equiv_apply, coe_mk, mul_apply, StandardEtalePresentation.toPresentation_σ', MulSemiringAction.toAlgEquiv_apply, Algebra.TensorProduct.piRight_tmul, matPolyEquiv_eval_eq_map, CliffordAlgebra.equivBaseChange_apply, restrictNormal_commutes, matPolyEquiv_coeff_apply, Matrix.piAlgEquiv_symm_apply, Module.Basis.tensorAlgebra_repr_apply, NumberField.InfinitePlace.comap_smul, IntermediateField.topEquiv_symm_apply_coe, MvPolynomial.optionEquivRight_apply, MvPolynomial.finSuccEquiv_apply, Ideal.coe_smul_primesOver_eq_map_galRestrict, Subalgebra.lTensorBot_tmul, MvPolynomial.tensorEquivSum_X_tmul_X, AddMonoidAlgebra.curryAlgEquiv_symm_single, prodUnique_apply, prodQuotientOfIsIdempotentElem_apply_snd, Subalgebra.topEquiv_symm_apply_coe, moduleEndSelf_apply_apply, FiniteGaloisIntermediateField.adjoin_simple_map_algEquiv, Quaternion.coe_starAe, IntermediateField.normal_iff_forall_map_eq', Localization.coe_algEquiv, AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ, MvPolynomial.algebraTensorAlgEquiv_symm_map, IntermediateField.intermediateFieldMap_apply_coe, rightInverse_symm, IntermediateField.topEquiv_apply, QuaternionAlgebra.imJ_swapEquiv_symm_apply, MvPolynomial.tensorEquivSum_C_tmul_one, ofLinearEquiv_symm, Matrix.toLinAlgEquiv_self, Matrix.kroneckerAlgEquiv_symm_apply, MvPolynomial.sumAlgEquiv_apply, PowerBasis.equivOfRoot_apply, Ideal.quotientKerAlgEquivOfSurjective_symm_apply, polyEquivTensor_apply, FreeLieAlgebra.universalEnvelopingEquivFreeAlgebra_symm_apply, LaurentPolynomial.invert_apply, Ideal.quotientKerAlgEquivOfSurjective_mk, CliffordAlgebraDualNumber.equiv_ι, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, ofLeftInverse_symm_apply, Subalgebra.LinearDisjoint.val_mulMap_tmul, minpoly.equivAdjoin_toAlgHom, RingCon.quotientKerEquivRangeₐ_mkₐ, GradedTensorProduct.comm_coe_tmul_coe, Algebra.TensorProduct.Algebra.TensorProduct.commRight_symm_tmul, AlgebraicIndependent.aevalEquivField_apply_coe, quotientBot_symm_mk, val_inv_algHomUnitsEquiv_symm_apply, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, moduleEndSelfOp_symm_apply, map_det, AlgebraicIndependent.aevalEquiv_apply_coe, Subalgebra.rTensorBot_symm_apply, StandardEtalePresentation.aeval_val_equivMvPolynomial, Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop_tmul, IsAdjoinRoot.lift_algEquiv, NumberField.IsCMField.complexConj_eq_self_iff, Polynomial.Bivariate.swap_C, Matrix.uniqueAlgEquiv_symm_apply, Matrix.transposeAlgEquiv_apply, MvPolynomial.pderiv_inr_universalFactorizationMap_X, MvPolynomial.sumAlgEquiv_symm_apply, Algebra.TensorProduct.tensorTensorTensorComm_tmul, exists_linearIndependent_algEquiv_apply, TensorAlgebra.equivDirectSum_symm_apply, algebraMap_eq_apply, MvPolynomial.eval₂_pUnitAlgEquiv_symm, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, QuaternionAlgebra.re_swapEquiv_apply, toLinearMap_apply, IntermediateField.coe_equivMap_apply, AddMonoidAlgebra.scalarTensorEquiv_symm_single, fieldRange_eq_top, prodQuotientOfIsIdempotentElem_apply_fst, Algebra.algebraMap_intNorm_of_isGalois, smul_units_def, Matrix.reindexAlgEquiv_apply, MonoidAlgebra.curryAlgEquiv_symm_single, comp_symm, Polynomial.toFinsuppIsoAlg_apply, minpoly.coe_equivAdjoin, MvPolynomial.optionEquivLeft_monomial, RatFunc.ofFractionRing_eq, Matrix.dualNumberEquiv_apply, opComm_symm_apply_apply, moduleEndSelf_symm_apply, FiniteField.frobeniusAlgEquiv_apply, Polynomial.aeval_algEquiv, galLiftEquiv_algebraMap_apply, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk, IsGalois.map_fixingSubgroup, support_subset_support_matPolyEquiv, Matrix.toLinAlgEquiv'_toMatrixAlgEquiv', Polynomial.algEquivAevalNegX_apply, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.optionEquivLeft_symm_apply, opComm_symm_apply_symm_apply, IsAdjoinRoot.ofAlgEquiv_map_apply, Matrix.kroneckerTMulAlgEquiv_apply, injective, MvPolynomial.algebraTensorAlgEquiv_tmul, Algebra.TensorProduct.comm_tmul, matPolyEquiv_symm_map_eval, CommAlgCat.isoMk_inv, endVecAlgEquivMatrixEnd_symm_apply_apply, MvPolynomial.mem_support_coeff_finSuccEquiv, linearEquivConj_mulRight, IsLocalization.algEquiv_symm_apply, Matrix.toLinAlgEquiv'_one, IntermediateField.botEquiv_def, Quaternion.re_snd_dualNumberEquiv, Polynomial.mapAlgEquiv_coe_ringHom, AdjoinRoot.quotEquivQuotMap_symm_apply, piCongrLeft_symm_apply, Algebra.TensorProduct.opAlgEquiv_tmul, StandardEtalePresentation.toPresentation_val, Polynomial.algEquivOfCompEqX_apply, matPolyEquiv_eval, mopMatrix_symm_apply, restrictNormalHom_apply, InfiniteGalois.mk_toAlgEquivAux, coe_fun_injective, liftNormal_commutes, MvPolynomial.pUnitAlgEquiv_monomial, Matrix.transposeAlgEquiv_symm_apply, ofAlgHom_apply, NumberField.IsCMField.RingOfIntegers.complexConj_eq_self_iff, AddMonoidAlgebra.domCongr_apply, Polynomial.algEquivCMulXAddC_symm_apply, coe_algHom_ofAlgHom, CliffordAlgebra.evenEquivEvenNeg_symm_apply, Algebra.TensorProduct.comm_comp_map, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, Quaternion.snd_imI_dualNumberEquiv_symm, IsPrimitiveRoot.autToPow_spec, RCLike.conjAe_coe, PowerBasis.equivOfRoot_aeval, InfiniteGalois.proj_of_le, Algebra.Generators.ofAlgEquiv_val, MvPolynomial.tensorEquivSum_one_tmul_X, AdjoinRoot.coe_algEquivOfEq, Differential.algEquiv_deriv', op_symm_apply_apply, piCongrRight_apply, AdjoinRoot.equiv'_apply, Algebra.TensorProduct.prodRight_tmul, Algebra.TensorProduct.prodRight_tmul_snd, Polynomial.algEquivAevalXAddC_apply, MvPolynomial.universalFactorizationMapPresentation_σ', Algebra.IsPushout.equiv_symm_algebraMap_right, MonoidAlgebra.domCongr_support, autEquivRootsOfUnity_apply_rootOfSplit, matPolyEquiv_symm_X, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, uniqueProd_apply, FractionalIdeal.map_map_symm, DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ, IsCyclotomicExtension.fromZetaAut_spec, Algebra.Presentation.quotientEquiv_mk, IsAdjoinRoot.algEquiv_root, IsAdjoinRoot.algEquiv_map, Module.Basis.toMatrix_reindex', MvPolynomial.esymmAlgEquiv_apply, LinearMap.toMatrixAlgEquiv_apply', trace_eq_sum_automorphisms, IsAdjoinRoot.liftHom_algEquiv, IsFractionRing.algEquiv_commutes, IntermediateField.equivOfEq_apply, algebraicClosure.map_eq_of_algEquiv, NumberField.IsCMField.infinitePlace_complexConj, MvPolynomial.optionEquivLeft_symm_C_X, IntermediateField.liftAlgEquiv_apply, NumberField.ComplexEmbedding.IsConj.comp, MvPolynomial.finSuccEquiv_X_zero, MvPolynomial.degreeOf_eq_natDegree, CliffordAlgebra.involuteEquiv_symm_apply, trans_apply, DoubleQuot.coe_quotQuotEquivCommₐ, FractionalIdeal.map_symm_map, SkewMonoidAlgebra.domCongr_single, Algebra.intNorm_map_algEquiv, StandardEtalePresentation.toPresentation_relation, prodUnique_symm_apply, invFun_eq_symm, QuaternionAlgebra.imJ_swapEquiv_apply, InfiniteGalois.limitToAlgEquiv_symm_apply, QuaternionAlgebra.imI_swapEquiv_apply, uniqueProd_symm_apply, AddMonoidAlgebra.scalarTensorEquiv_tmul, separableClosure.map_eq_of_algEquiv, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, Polynomial.residueFieldMapCAlgEquiv_symm_X, coe_algEquiv_lpBCF_symm, MvPolynomial.algebraTensorAlgEquiv_symm_monomial, spectralNorm_eq_of_equiv, LinearMap.toMatrixAlgEquiv_reindexRange, MvPolynomial.optionEquivLeft_elim_eval, MvPolynomial.optionEquivLeft_symm_X, WithLp.unitizationAlgEquiv_apply, sumArrowEquivProdArrow_apply, subalgebraMap_symm_apply_coe, matPolyEquiv_coeff_apply_aux_2, funUnique_symm_apply, Algebra.TensorProduct.piScalarRight_tmul_apply, Algebra.TensorProduct.lidOfCompatibleSMul_tmul, MvPolynomial.supportedEquivMvPolynomial_symm_C, IsAdjoinRoot.ofAlgEquiv_root, bijective, IsSymmetricAlgebra.equiv_toAlgHom, MvPolynomial.tensorEquivSum_X_tmul_one, MvPolynomial.eval₂_pUnitAlgEquiv, Ideal.relNorm_map_algEquiv, matPolyEquiv_smul_one, autAdjoinRootXPowSubC_root, LinearMap.toMatrixAlgEquiv_mul, matrixEquivTensor_apply, ContinuousAlgEquiv.coe_mk, toLieEquiv_apply, Algebra.TensorProduct.opAlgEquiv_symm_tmul, toAlgHom_apply, LaurentPolynomial.toLaurent_reverse, Subalgebra.mopAlgEquivOp_apply_coe, addMonoidAlgebraAlgEquivDirectSum_apply, prodCongr_symm_apply, surjective, MvPolynomial.optionEquivLeft_symm_C_C, matPolyEquiv_eq_X_pow_sub_C, Subalgebra.algEquivOpMop_symm_apply_coe, Algebra.TensorProduct.lid_symm_apply, RingCon.quotientQuotientEquivQuotientₐ_coe_coe, ofBijective_apply_symm_apply, opOp_symm_apply, Algebra.TensorProduct.leftComm_symm_tmul, MvPolynomial.tensorEquivSum_C_tmul_C, MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, IntermediateField.mem_fixingSubgroup_iff, Subalgebra.rTensorBot_tmul, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, IntermediateField.intermediateFieldMap_symm_apply_coe, CliffordAlgebra.reverseOpEquiv_apply, Matrix.toLpLinAlgEquiv_symm_apply, LaurentPolynomial.invert_C, piCongrLeft'_symm_apply, AddMonoidAlgebra.curryAlgEquiv_single, NumberField.IsCMField.complexConj_torsion, Polynomial.residueFieldMapCAlgEquiv_algebraMap, Polynomial.Bivariate.equivMvPolynomial_C_C, RatFunc.toFractionRingAlgEquiv_apply, CliffordAlgebra.equivOfIsometry_apply, ofRingEquiv_symm_apply, Algebra.TensorProduct.rid_symm_apply, LinearMap.toMatrixAlgEquiv_transpose_apply, Matrix.piAlgEquiv_apply, MonoidAlgebra.domCongr_apply, Quaternion.fst_re_dualNumberEquiv_symm, coe_algEquiv_lpBCF, coe_restrictScalars_symm', Quaternion.imI_snd_dualNumberEquiv, Equiv.algEquiv_symm_apply, QuaternionAlgebra.imK_swapEquiv_apply, polyEquivTensor_symm_apply_tmul_eq_smul, Differential.algEquiv_deriv, IsAdjoinRoot.algEquiv_apply_map, PowerBasis.equivOfRoot_gen, coe_coe, congr_fun, Matrix.toLinAlgEquiv_toMatrixAlgEquiv, NumberField.IsCMField.Units.complexConj_eq_self_iff, coe_trans, LaurentPolynomial.invert_comp_C, MvPolynomial.totalDegree_coeff_optionEquivLeft_le, Algebra.botEquiv_symm_apply, LinearMap.toMatrixAlgEquiv_transpose_apply', MonoidAlgebra.curryAlgEquiv_single, Polynomial.residueFieldMapCAlgEquiv_symm_C, algHomUnitsEquiv_apply_apply, RingCon.coe_quotientKerEquivRangeₐ_mkₐ, StandardEtalePresentation.equivRing_symm_X, Ideal.relNorm_comap_algEquiv, extendScalarsOfSurjective_apply, NumberField.ComplexEmbedding.exists_comp_symm_eq_of_comp_eq, IsGalois.mem_bot_iff_fixed, MvPolynomial.esymmAlgEquiv_symm_apply, Shrink.algEquiv_symm_apply, LinearMap.toMatrixAlgEquiv'_comp, congr_arg, LaurentPolynomial.invert_T, MvPolynomial.commAlgEquiv_C_X, Polynomial.coe_mapAlgEquiv, Localization.coe_algEquiv_symm, MvPolynomial.renameSymmetricSubalgebra_apply_coe, mapMatrix_apply, Quaternion.imK_snd_dualNumberEquiv, prod_galRestrict_eq_norm, coe_ringHom_commutes, LaurentPolynomial.involutive_invert, MvPolynomial.eval_polynomial_eval_finSuccEquiv, MvPolynomial.pderiv_inl_universalFactorizationMap_X, autEquivRootsOfUnity_smul, Localization.algEquiv_symm_apply, toAlgebraIso_hom, AdjoinRoot.coe_algEquivOfAssociated, AdicCompletion.ofAlgEquiv_symm_of, RatFunc.toFractionRing_eq, toLinearEquiv_apply
|
instInhabited 📖 | CompOp | — |
instMulDistribMulActionUnits 📖 | CompOp | 2 mathmath: groupCohomology.norm_ofAlgebraAutOnUnits_eq, smul_units_def
|
ofAlgHom 📖 | CompOp | 6 mathmath: toLinearMap_ofAlgHom, ofAlgHom_symm_apply, ofAlgHom_coe_algHom, ofAlgHom_symm, ofAlgHom_apply, coe_algHom_ofAlgHom
|
ofBijective 📖 | CompOp | 7 mathmath: ofBijective_symm_apply_apply, ofBijective_apply, toAlgHom_ofBijective, coe_ofBijective, Algebra.IsAlgebraic.algEquivEquivAlgHom_symm_apply, toLinearMap_ofBijective, ofBijective_apply_symm_apply
|
ofLinearEquiv 📖 | CompOp | 4 mathmath: ofLinearEquiv_toLinearEquiv, toLinearEquiv_ofLinearEquiv, ofLinearEquiv_apply, ofLinearEquiv_symm
|
ofRingEquiv 📖 | CompOp | 4 mathmath: ofRingEquiv_apply, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, ofRingEquiv_toEquiv, ofRingEquiv_symm_apply
|
refl 📖 | CompOp | 30 mathmath: piCongrRight_refl, refl_toRingHom, Polynomial.mapAlgEquiv_id, self_trans_symm, CliffordAlgebra.equivOfIsometry_refl, coe_refl, aut_one, AddMonoidAlgebra.domCongr_refl, IntermediateField.equivOfEq_rfl, StarAlgEquiv.toAlgEquiv_refl, IsFractionRing.fieldEquivOfAlgEquiv_refl, mapMatrix_refl, MvPolynomial.mapAlgEquiv_refl, IsAdjoinRoot.algEquiv_self, SkewMonoidAlgebra.domCongr_refl, Subalgebra.equivOfEq_rfl, autCongr_refl, Algebra.TensorProduct.congr_refl, MvPolynomial.renameEquiv_refl, refl_toAlgHom, opComm_apply_symm_apply, Matrix.reindexAlgEquiv_refl, refl_symm, opComm_symm_apply_symm_apply, equivCongr_refl, FractionalIdeal.mapEquiv_refl, symm_trans_self, arrowCongr_refl, toLinearEquiv_refl, MonoidAlgebra.domCongr_refl
|
toAddEquiv 📖 | CompOp | — |
toAlgHom 📖 | CompOp | 48 mathmath: AlgCat.hom_inv_associator, CommAlgCat.braiding_hom_hom, AddMonoidAlgebra.domCongr_toAlgHom, MonoidAlgebra.domCongr_toAlgHom, AlgCat.hom_inv_rightUnitor, Bialgebra.TensorProduct.counitAlgHom_def, RingCon.quotientKerEquivRangeₐ_comp_mkₐ, toAlgHom_op, toAlgHom_eq_coe, Bialgebra.TensorProduct.comul_eq_algHom_toLinearMap, arrowCongr_apply, MvPolynomial.sumAlgEquiv_comp_rename_inr, Normal.algHomEquivAut_symm_apply, Bialgebra.TensorProduct.counit_eq_algHom_toLinearMap, AlgCat.hom_hom_associator, Bialgebra.TensorProduct.comulAlgHom_def, Subalgebra.mulMap_bot_left_eq, AdjoinRoot.equiv'_symm_toAlgHom, SkewMonoidAlgebra.domCongrAlg_toAlgHom, IsAzumaya.mulLeftRight_comp_congr, MvPolynomial.sumAlgEquiv_comp_rename_inl, AlgCat.hom_hom_rightUnitor, MvPolynomial.rename_esymmAlgHom, AlgCat.hom_inv_leftUnitor, AdjoinRoot.equiv'_toAlgHom, AlgCat.hom_hom_leftUnitor, AdjoinRoot.algEquivOfAssociated_toAlgHom, Subalgebra.mulMap_bot_right_eq, CliffordAlgebra.toBaseChange_comp_reverseOp, coe_algHom, CommAlgCat.braiding_inv_hom, CommAlgCat.associator_inv_hom, Algebra.TensorProduct.algEquivIncludeRange_toAlgHom, DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ, StandardEtalePresentation.toPresentation_σ', toAlgHom_unop, IntermediateField.intermediateFieldMap_apply_coe, Algebra.IsAlgebraic.algEquivEquivAlgHom_apply, ContinuousAlgEquiv.comp_coe, Algebra.TensorProduct.algEquivIncludeRange_symm_toAlgHom, Algebra.TensorProduct.comm_comp_map, CommAlgCat.associator_hom_hom, perfectClosure.map_eq_of_algEquiv, Algebra.TensorProduct.lmul''_eq_lid_comp_mapOfCompatibleSMul, toAlgHomHom_apply, toAlgHom_apply, AdjoinRoot.algEquivOfEq_toAlgHom, IntermediateField.intermediateFieldMap_symm_apply_coe
|
toAlgHomHom 📖 | CompOp | 1 mathmath: toAlgHomHom_apply
|
toEquiv 📖 | CompOp | 9 mathmath: StarAlgEquiv.ofInjective_symm_apply, ContinuousAlgEquiv.continuous_invFun, ContinuousAlgEquiv.continuous_toFun, map_add', toEquiv_eq_coe, map_mul', invFun_eq_symm, commutes', BialgEquiv.ofAlgEquiv_apply
|
toLinearEquiv 📖 | CompOp | 27 mathmath: linearEquivConj_mulLeft, PowerBasis.map_basis, toLinearEquiv_toOpposite, RCLike.conjCLE_coe, toLinearEquiv_ofLinearEquiv, toLinearEquiv_symm, IsAzumaya.mulLeftRight_comp_congr, Algebra.TensorProduct.congr_toLinearEquiv, coe_symm_toLinearEquiv, Algebra.TensorProduct.toLinearEquiv_tensorTensorTensorComm, Algebra.TensorProduct.assoc_toLinearEquiv, Complex.linearEquiv_det_conjAe, linearEquivConj_mulLeftRight, coe_toLinearEquiv, Algebra.TensorProduct.tensorTensorTensorComm_toLinearEquiv, toLinearEquiv_toLinearMap, ContinuousAlgEquiv.toContinuousLinearEquiv_toLinearEquiv_eq, linearEquivConj_mulRight, Algebra.TensorProduct.rid_toLinearEquiv, Matrix.toLinearEquiv_kroneckerAlgEquiv, toLinearEquiv_refl, toLinearEquiv_injective, Algebra.TensorProduct.lid_toLinearEquiv, toLinearEquiv_trans, Algebra.TensorProduct.comm_toLinearEquiv, Complex.conjCLE_coe, toLinearEquiv_apply
|
toLinearMap 📖 | CompOp | 17 mathmath: AddMonoidAlgebra.domCongr_comp_lsingle, pow_toLinearMap, trans_toLinearMap, toLinearMap_ofAlgHom, toLinearMap_injective, toAlgHom_toLinearMap, Complex.det_conjAe, map_equiv_traceDual, MonoidAlgebra.domCongr_comp_lsingle, one_toLinearMap, toLinearEquiv_toLinearMap, minpoly_algEquiv_toLinearMap, toLinearMap_apply, Complex.toMatrix_conjAe, toLinearMap_ofBijective, IsSymmetricAlgebra.comp_equiv, Submodule.map_div
|
toLinearMapHom 📖 | CompOp | 1 mathmath: toLinearMapHom_apply_apply
|
toMulEquiv 📖 | CompOp | — |
toRingEquiv 📖 | CompOp | 13 mathmath: coe_ringEquiv', IsLocalization.algEquivOfAlgEquiv_apply, DifferentialAlgebra.equiv, toRingEquiv_unop, Algebra.WeaklyQuasiFiniteAt.comap_algEquiv, IsLocalization.algEquivOfAlgEquiv_symm_apply, subalgebraMap_apply_coe, toRingEquiv_op, RatFunc.toFractionRingRingEquiv_symm_eq, Algebra.QuasiFiniteAt.comap_algEquiv, ModuleCat.Algebra.restrictScalarsEquivalenceOfRingEquiv_linear, AlgebraicGeometry.localRingHom_comp_stalkIso, toRingEquiv_eq_coe
|
trans 📖 | CompOp | 38 mathmath: Algebra.TensorProduct.congr_trans, AddMonoidAlgebra.mapRangeAlgEquiv_trans, restrictNormal_trans, self_trans_symm, piCongrRight_trans, CliffordAlgebra.equivOfIsometry_trans, IsFractionRing.fieldEquivOfAlgEquiv_trans, Subalgebra.comm_trans_rTensorBot, ContinuousAlgEquiv.trans_toAlgEquiv, MvPolynomial.renameEquiv_trans, trans_toLinearMap, MonoidAlgebra.mapRangeAlgEquiv_trans, equivCongr_apply, toUnder_trans, Polynomial.mapAlgEquiv_comp, symm_trans_apply, IsAdjoinRoot.algEquiv_def, StarAlgEquiv.toAlgEquiv_trans, opComm_apply_symm_apply, toRingHom_trans, autCongr_apply, MvPolynomial.mapAlgEquiv_trans, arrowCongr_trans, IsAdjoinRoot.algEquiv_trans, IsAdjoinRoot.algEquiv_ofAlgEquiv, opComm_symm_apply_symm_apply, IsAdjoinRoot.ofAlgEquiv_algEquiv, mapMatrix_trans, Subalgebra.comm_trans_lTensorBot, trans_apply, symm_trans_self, aut_mul, IntermediateField.equivOfEq_trans, equivCongr_trans, toLinearEquiv_trans, coe_trans, autCongr_trans, Subalgebra.equivOfEq_trans
|