Basic

📁 Source: Mathlib/Algebra/Algebra/Basic.lean

Statistics

Metric	Count
Definitions algebraMapSubmonoid, instSubtypeMemSubringCenter, ofSubring, ofSubsemiring, semiringToRing, algebraMapOfInvertibleAlgebraMap, extendScalarsOfSurjective, extendScalarsOfSurjective, extendScalarsOfSurjectiveEquiv, instAlgebra, algebra, toIntAlgebra, commSemiringToCommRing, toNatAlgebra, algebra	15
Theorems algebraMapSubmonoid_powers, algebraMapSubmonoid_self, algebraMap_ofSubring, algebraMap_ofSubring_apply, algebraMap_ofSubsemiring, algebraMap_ofSubsemiring_apply, algebraMap_pUnit, charZero_of_charZero, coe_algebraMap_ofSubring, coe_algebraMap_ofSubsemiring, mem_algebraMapSubmonoid_of_mem, mul_sub_algebraMap_commutes, mul_sub_algebraMap_pow_commutes, to_smulCommClass, algebraMap_eq_one_iff, algebraMap_eq_zero_iff, algebraMap_injective, to_isTorsionFree, of_faithfulSMul, of_faithfulSMul, to_smulCommClass, to_smulCommClass', algebraMap_of_algebraMap, extendScalarsOfSurjective_apply, extendScalarsOfSurjective_symm, extendScalarsOfSurjective_apply, map_algebraMap_mul, map_mul_algebraMap, algebraMap_isUnit_inv_apply_eq_iff, algebraMap_isUnit_inv_apply_eq_iff', of_faithfulSMul, to_faithfulSMul, trans_faithfulSMul, algebraMap_end_apply, algebraMap_end_eq_smul_id, isTorsionFree_iff_algebraMap_injective, isTorsionFree_iff_faithfulSMul, ker_algebraMap_end, of_faithfulSMul, of_faithfulSMul, iff_algebraMap_injective, iff_faithfulSMul, algebraMap_eq, down_algebraMap, coe_eq_zero_iff, coe_inj, coe_prod, coe_sum, lift_map_eq_zero_iff, algebraMap_comp_intCast, algebraMap_comp_natCast, algebraMap_int_eq, algebraMap_smul, algebra_compatible_smul, bijective_algebraMap_of_linearEquiv, bijective_algebraMap_of_linearMap, faithfulSMul_iff_algebraMap_injective, injective_algebraMap_of_linearMap, instFaithfulSMulIntOfCharZero, instFaithfulSMulNatOfCharZero, instSMulCommClass, int_algebra_subsingleton, isSMulRegular_algebraMap_iff, nat_algebra_subsingleton, smul_algebra_smul_comm, surjective_algebraMap_of_linearMap	66
Total	81

Algebra

Definitions

Name	Category	Theorems
algebraMapSubmonoid 📖	CompOp	57 math math: IsLocalization.algebraMap_apply_eq_map_map_submonoid, algebraMapSubmonoid_map_map, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl, isIntegral_localization, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, IsLocalization.mk'_tmul, instIsLocalizationAlgebraMapSubmonoidPrimeComplLocalization, IsIntegralClosure.isLocalization, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, IsLocalization.commutes, instIsSeparableFractionRingLocalizationAlgebraMapSubmonoidPrimeCompl, instIsScalarTowerAtPrimeLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, IsLocalizedModule.of_restrictScalars, NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, AlgHom.toKerIsLocalization_apply, IsLocalization.mk'_algebraMap_eq_mk', isLocalizedModule_iff_isLocalization, IsLocalization.Away.instAlgebraMapSubmonoidPowersOfCoeRingHomAlgebraMap, instIsPrincipalIdealRingLocalizationAlgebraMapSubmonoidPrimeComplOfIsDedekindDomainOfFiniteOfNeZeroIdeal, algebraMapSubmonoid_le_comap, algebraMapSubmonoid_map_eq, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_1, Localization.instIsTorsionFreeAtPrimeAlgebraMapSubmonoidPrimeComplOfIsDomain, IsAlgebraic.instIsLocalizationAlgebraMapSubmonoidNonZeroDivisors, instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl, instFiniteAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, instFiniteFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, IsLocalization.tmul_mk', instIsSeparableFractionRingAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, localizationAlgebraMap_def, instFiniteLocalizationAlgebraMapSubmonoidPrimeCompl, IsLocalization.mapₐ_coe, Ideal.disjoint_primeCompl_of_liesOver, IsLocalization.tensorRight, IsLocalization.tensor, IsLocalization.integralClosure, IsLocalization.isLocalization_algebraMapSubmonoid_map_algHom, IsLocalization.algebraMap_mk', instIsTorsionFreeLocalizationAlgebraMapSubmonoidPrimeCompl_2, instIsScalarTowerLocalizationAlgebraMapSubmonoid, AlgHom.toKerIsLocalization_isLocalizedModule, algebraMapSubmonoid_powers, IsLocalization.instIsDomainLocalizationAlgebraMapSubmonoidPrimeComplOfFaithfulSMul, instIsDedekindDomainLocalizationAlgebraMapSubmonoidPrimeCompl, algebraMapSubmonoid_self, instIsLocalizationAlgebraMapSubmonoid, instIsFractionRingLocalizationAlgebraMapSubmonoidPrimeComplFractionRing, IsLocalization.tensorProduct_tensorProduct, instIsScalarTowerLocalizationAlgebraMapSubmonoidPrimeCompl_1, instIsIntegralAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, mem_algebraMapSubmonoid_of_mem, algebraMapSubmonoid_le_nonZeroDivisors_of_faithfulSMul, is_integral_localization_at_leadingCoeff, IsIntegralClosure.isLocalization_of_isSeparable, isLocalization_iff_isPushout, IsLocalization.algebraMap_eq_map_map_submonoid
instSubtypeMemSubringCenter 📖	CompOp	2 math math: JacobsonNoether.exist_pow_eq_zero_of_le, JacobsonNoether.exists_separable_and_not_isCentral
ofSubring 📖	CompOp	11 math math: coe_algebraMap_ofSubring, instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure, toSubring_bot, iInf_valuationSubring_superset, Polynomial.int_eval₂_eq, algebraMap_ofSubring, Polynomial.map_restriction, minpoly.ofSubring, isIntegral_iff_isIntegral_closure_finite, minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure, algebraMap_ofSubring_apply
ofSubsemiring 📖	CompOp	8 math math: IsUnramifiedAt.exists_primesOver_under_adjoin_eq_singleton_and_residueField_bijective, algebraMap_ofSubsemiring_apply, coe_algebraMap_ofSubsemiring, Subring.integralClosure_subring_le_iff, Valuation.HasExtension.instIsScalarTower_valuationSubring', algebraMap_ofSubsemiring, Valuation.HasExtension.instIsScalarTower_valuationSubring, Subring.isIntegrallyClosedIn_iff
semiringToRing 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMapSubmonoid_powers 📖	mathematical	—	algebraMapSubmonoid Submonoid.powers MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	Submonoid.map_powers
algebraMapSubmonoid_self 📖	mathematical	—	algebraMapSubmonoid CommSemiring.toSemiring id	—	Submonoid.map_id
algebraMap_ofSubring 📖	mathematical	—	algebraMap Subring CommRing.toRing SetLike.instMembership Subring.instSetLike SubsemiringClass.toCommSemiring CommRing.toCommSemiring SubringClass.toSubsemiringClass Subring.instSubringClass CommSemiring.toSemiring ofSubring id Subring.subtype	—	SubringClass.toSubsemiringClass Subring.instSubringClass
algebraMap_ofSubring_apply 📖	mathematical	—	DFunLike.coe RingHom Subring CommRing.toRing SetLike.instMembership Subring.instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring CommRing.toCommSemiring SubringClass.toSubsemiringClass Subring.instSubringClass RingHom.instFunLike algebraMap ofSubring id	—	SubringClass.toSubsemiringClass Subring.instSubringClass
algebraMap_ofSubsemiring 📖	mathematical	—	algebraMap Subsemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring SetLike.instMembership Subsemiring.instSetLike Subsemiring.toCommSemiring ofSubsemiring id Subsemiring.instSubsemiringClass Subsemiring.subtype	—	Subsemiring.instSubsemiringClass
algebraMap_ofSubsemiring_apply 📖	mathematical	—	DFunLike.coe RingHom SetLike.instMembership Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring RingHom.instFunLike algebraMap ofSubsemiring id	—	—
algebraMap_pUnit 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring PUnit.commRing RingHom.instFunLike algebraMap PUnit.algebra	—	—
charZero_of_charZero 📖	mathematical	—	CharZero AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring	—	algebraMap_comp_natCast FaithfulSMul.algebraMap_injective CharZero.cast_injective
coe_algebraMap_ofSubring 📖	mathematical	—	DFunLike.coe RingHom Subring CommRing.toRing SetLike.instMembership Subring.instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring CommRing.toCommSemiring SubringClass.toSubsemiringClass Subring.instSubringClass RingHom.instFunLike algebraMap ofSubring id	—	SubringClass.toSubsemiringClass Subring.instSubringClass
coe_algebraMap_ofSubsemiring 📖	mathematical	—	DFunLike.coe RingHom SetLike.instMembership Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring RingHom.instFunLike algebraMap ofSubsemiring id	—	—
mem_algebraMapSubmonoid_of_mem 📖	mathematical	—	Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike algebraMapSubmonoid DFunLike.coe RingHom CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Set.mem_image_of_mem
mul_sub_algebraMap_commutes 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Ring.toSemiring RingHom.instFunLike algebraMap	—	mul_sub commutes sub_mul
mul_sub_algebraMap_pow_commutes 📖	mathematical	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Ring.toSemiring SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	pow_zero mul_one one_mul pow_succ' mul_assoc mul_sub_algebraMap_commutes
to_smulCommClass 📖	mathematical	—	SMulCommClass toSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring	—	IsScalarTower.to_smulCommClass IsScalarTower.right

FaithfulSMul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_eq_one_iff 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_eq_one_iff MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_injective
algebraMap_eq_zero_iff 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring	—	map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap_injective
algebraMap_injective 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	faithfulSMul_iff_algebraMap_injective
to_isTorsionFree 📖	mathematical	—	Module.IsTorsionFree CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule	—	Module.IsTorsionFree.trans_faithfulSMul instIsTorsionFree IsScalarTower.right

Invertible

Definitions

Name	Category	Theorems
algebraMapOfInvertibleAlgebraMap 📖	CompOp	—

IsCancelMulZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_faithfulSMul 📖	mathematical	—	IsCancelMulZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Function.Injective.isCancelMulZero FaithfulSMul.algebraMap_injective map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass

IsDomain

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_faithfulSMul 📖	mathematical	—	IsDomain CommSemiring.toSemiring	—	Function.Injective.isDomain RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass FaithfulSMul.algebraMap_injective

IsScalarTower

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
to_smulCommClass 📖	mathematical	—	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction	—	algebra_compatible_smul smul_smul Algebra.commutes SemigroupAction.mul_smul
to_smulCommClass' 📖	mathematical	—	SMulCommClass SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction CommSemiring.toSemiring	—	SMulCommClass.symm to_smulCommClass

IsUnit

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_of_algebraMap 📖	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule LinearMap.instFunLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom RingHom.instFunLike algebraMap	—	—	nonempty_invertible isUnit_of_invertible

LinearEquiv

Definitions

Name	Category	Theorems
extendScalarsOfSurjective 📖	CompOp	2 math math: extendScalarsOfSurjective_symm, extendScalarsOfSurjective_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendScalarsOfSurjective_apply 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	LinearEquiv RingHom.id RingHomInvPair.ids EquivLike.toFunLike instEquivLike extendScalarsOfSurjective	—	RingHomInvPair.ids
extendScalarsOfSurjective_symm 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	symm RingHom.id RingHomInvPair.ids extendScalarsOfSurjective	—	RingHomInvPair.ids

LinearMap

Definitions

Name	Category	Theorems
extendScalarsOfSurjective 📖	CompOp	1 math math: extendScalarsOfSurjective_apply
extendScalarsOfSurjectiveEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
extendScalarsOfSurjective_apply 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	LinearMap RingHom.id instFunLike extendScalarsOfSurjective	—	—
map_algebraMap_mul 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap	—	Algebra.smul_def map_smul SemilinearMapClass.toMulActionSemiHomClass semilinearMapClass
map_mul_algebraMap 📖	mathematical	—	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule instFunLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib RingHom RingHom.instFunLike algebraMap	—	Algebra.commutes map_algebraMap_mul

Module

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_end_apply 📖	mathematical	—	DFunLike.coe End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring RingHom CommSemiring.toSemiring End.instSemiring RingHom.instFunLike algebraMap End.instAlgebra SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero toDistribMulAction	—	—
algebraMap_end_eq_smul_id 📖	mathematical	—	DFunLike.coe RingHom End Semiring.toNonAssocSemiring CommSemiring.toSemiring End.instSemiring RingHom.instFunLike algebraMap End.instAlgebra LinearMap RingHom.id LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid toDistribMulAction LinearMap.id	—	—
isTorsionFree_iff_algebraMap_injective 📖	mathematical	—	IsTorsionFree CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	isTorsionFree_iff_faithfulSMul faithfulSMul_iff_algebraMap_injective
isTorsionFree_iff_faithfulSMul 📖	mathematical	—	IsTorsionFree CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring FaithfulSMul Algebra.toSMul	—	IsTorsionFree.to_faithfulSMul IsDomain.toIsCancelMulZero IsDomain.toNontrivial FaithfulSMul.to_isTorsionFree
ker_algebraMap_end 📖	mathematical	—	LinearMap.ker DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring DFunLike.coe RingHom End CommSemiring.toSemiring Semifield.toCommSemiring End.instSemiring RingHom.instFunLike algebraMap End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid toDistribMulAction Algebra.toSMul Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero Bot.bot Submodule Submodule.instBot	—	LinearMap.ker_smul

Module.End

Definitions

Name	Category	Theorems
instAlgebra 📖	CompOp	268 math math: Matrix.toLinAlgEquiv_one, AlgEquiv.moduleEndSelfOp_apply_apply, LinearMap.toMatrixAlgEquiv'_mul, LinearMap.exists_monic_and_aeval_eq_zero, LinearMap.BilinForm.isSkewAdjoint_bracket, HasEigenvalue.mem_spectrum, LieModule.toEnd_pow_apply_map, Polynomial.disjoint_ker_aeval_of_isCoprime, PolynomialModule.smul_def, Matrix.spectrum_toEuclideanLin, LieModule.trace_toEnd_eq_zero_of_mem_lcs, LieAlgebra.mapsTo_toEnd_genWeightSpace_add_of_mem_rootSpace, LinearMap.toMatrixAlgEquiv_comp, Representation.asAlgebraHom_single, LieAlgebra.finrank_engel, skewAdjointLieSubalgebraEquiv_apply, Algebra.lmul_algebraMap, LinearEquiv.conjAlgEquiv_symm_apply_apply, spectrum_intrinsicStar, Matrix.spectrum_toLpLin, LieAlgebra.isRegular_iff_natTrailingDegree_charpoly_eq_rank, LieModule.exists_genWeightSpace_zero_le_ker_of_isNoetherian, isFinitelySemisimple_sub_algebraMap_iff, LieSubalgebra.toEnd_eq, Rep.to_Module_monoidAlgebra_map_aux, LieModule.isNilpotent_toEnd_genWeightSpace_zero, minpoly_algHom_toLinearMap, LinearMap.toMatrixAlgEquiv_toLinAlgEquiv, IsLocalizedModule.iso_apply_mk, skewAdjointLieSubalgebraEquiv_symm_apply, Algebra.lmul_injective, LinearMap.spectrum_toMatrix', LieModule.trace_toEnd_genWeightSpace, Algebra.IsCentral.instEnd, AlgHom.mulLeftRightMatrix.inv_comp, LieModule.shiftedGenWeightSpace.toEnd_eq, Module.endTensorEndAlgHom_apply, Representation.asAlgebraHom_def, instLieModule, LieSubmodule.Quotient.toEnd_comp_mk', LinearMap.toMatrixAlgEquiv'_id, LinearEquiv.conjAlgEquiv_apply, LieModule.instIsTriangularizableSubtypeEndMemLieSubalgebraRangeToEnd, Module.AEval'.X_smul_of, LieModule.mem_posFittingCompOf, LocalizedModule.divBy_mul_by, LieModule.isNilpotent_range_toEnd_iff, LieAlgebra.rank_le_natTrailingDegree_charpoly_ad, LinearMap.toMatrixAlgEquiv_apply, LieSubmodule.lie_top_eq_of_span_sup_eq_top, LieAlgebra.ad_eq_lmul_left_sub_lmul_right, Matrix.toLinAlgEquiv_mul, LieModule.isNilpotent_toEnd_of_isNilpotent, LieAlgebra.hasCentralRadical_and_of_isIrreducible_of_isFaithful, LieSubmodule.coe_map_toEnd_le, Module.AEval'.of_symm_X_smul, LieModule.mem_genWeightSpace, LinearMap.detAux_def, LinearMap.toMatrixAlgEquiv_id, LieSubalgebra.toEnd_mk, Matrix.isRepresentation.toEnd_represents, LieModule.exists_genWeightSpace_le_ker_of_isNoetherian, hasUnifEigenvalue_iff_mem_spectrum, LieModule.coe_genWeightSpaceOf_zero, LinearEquiv.symm_conjAlgEquiv, IsSimpleModule.algebraMap_end_bijective_of_isAlgClosed, LieAlgebra.engel_isBot_of_isMin.lieCharpoly_map_eval, LieSubmodule.traceForm_eq_zero_of_isTrivial, lieEquivMatrix'_apply, LieModule.weight_vector_multiplication, LinearMap.minpoly_toMatrix', LieSubalgebra.coe_ad_pow, isLocalizedModule_iff, LinearMap.pow_eq_aeval_mod_charpoly, LinearMap.tensorProductEnd_apply, Module.AEval'.X_pow_smul_of, RootPairing.GeckConstruction.trace_toEnd_eq_zero, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, rTensorAlgHom_apply_apply, LieModule.isFaithful_iff, IsAzumaya.mulLeftRight_comp_congr, Polynomial.sup_aeval_range_eq_top_of_isCoprime, LieSubmodule.toEnd_comp_subtype_mem, LinearMap.minpoly_dvd_charpoly, LieAlgebra.ad_nilpotent_of_nilpotent, AlgHom.mulLeftRight_apply, Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime, LieModule.rank_eq_natTrailingDegree, aeval_apply_of_hasEigenvector, IsAzumaya.bij, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, LinearMap.toMatrixAlgEquiv'_apply, LieAlgebra.ad_pow_lie, LinearMap.toMatrix'_algebraMap, LieModule.isNilpotent_toEnd_of_isNilpotent₂, LieSubmodule.mapsTo_pow_toEnd_sub_algebraMap, IsLocalizedModule.fromLocalizedModule_mk, Derivation.commutator_coe_linear_map, isSemisimple_sub_algebraMap_iff, Polynomial.aeval_apply_smul_mem_of_le_comap, Matrix.isRepresentation.toEnd_exists_mem_ideal, Representation.asAlgebraHom_single_one, LieModule.exists_forall_pow_toEnd_eq_zero, JacobsonNoether.exist_pow_eq_zero_of_le, IsSemisimple.aeval, Algebra.lsmul_injective, LieSubmodule.toEnd_restrict_eq_toEnd, LieModule.IsFaithful.injective_toEnd, Module.algebraMap_end_eq_smul_id, LieModule.trace_comp_toEnd_genWeightSpace_eq, killingForm_apply_apply, LinearMap.toMatrix_algebraMap, LinearMap.spectrum_toMatrix, LieSubalgebra.mem_engel_iff, LieModule.iterate_toEnd_mem_lowerCentralSeries₂, Matrix.toLinAlgEquiv'_apply, LinearMap.aeval_eq_aeval_mod_charpoly, LinearMap.hasEigenvalue_zero_tfae, Matrix.minpoly_toLin', IsSl2Triple.HasPrimitiveVectorWith.pow_toEnd_f_eq_zero_of_eq_nat, LieModule.toEnd_eq_iff, LinearEquiv.lieConj_apply, LieModule.isNilpotent_toEnd_of_mem_rootSpace, LinearMap.toMatrixAlgEquiv'_toLinAlgEquiv', LieDerivation.toLinearMapLieHom_injective, IsAzumaya.coe_tensorEquivEnd, LinearMap.eval_charpoly, LieModule.toEnd_lie, isRoot_of_hasEigenvalue, LinearMap.toMatrixAlgEquiv_symm, IsSimpleRing.exists_algEquiv_matrix_end_mulOpposite, LinearMap.minpoly_toMatrix, Representation.asAlgebraHom_of, LinearMap.prodMapAlgHom_apply_apply, Algebra.toMatrix_lmul', LieAlgebra.ad_apply, LieAlgebra.toEnd_pow_apply_mem, LieAlgebra.conj_ad_apply, RestrictScalars.lsmul_apply_apply, LinearEquiv.conjAlgEquiv_apply_apply, finite_spectrum, endVecAlgEquivMatrixEnd_apply_apply, LinearMap.aeval_self_charpoly, LieModule.isRegular_iff_natTrailingDegree_charpoly_eq_rank, Module.algebraMap_end_apply, Ideal.constr_basisSpanSingleton, IsSl2Triple.HasPrimitiveVectorWith.lie_f_pow_toEnd_f, LieDerivation.commutator_coe_linear_map, Matrix.spectrum_toLin, Module.AEval.mem_mapSubmodule_symm_apply, LieModule.toEnd_pow_lie, LieSubmodule.coe_toEnd, LieModule.toEnd_apply_apply, LieModule.commute_toEnd_of_mem_center_right, IsSemisimpleModule.exists_end_algEquiv, Matrix.toLpLinAlgEquiv_apply_apply_ofLp, LieModule.toEnd_baseChange, LocalizedModule.mul_by_divBy, IsBaseChange.map_id_lsmul_eq_lsmul_algebraMap, Matrix.toLinAlgEquiv_apply, eigenspace_div, Polynomial.span_minpoly_eq_annihilator, LieModule.isNilpotent_iff_forall, LieModule.isNilpotent_toEnd_sub_algebraMap, lieEquivMatrix'_symm_apply, isNilpotent_tensor_residueField_iff, Polynomial.sup_ker_aeval_le_ker_aeval_mul, IsSl2Triple.HasPrimitiveVectorWith.lie_e_pow_succ_toEnd_f, Algebra.toMatrix_lsmul, AlgEquiv.moduleEndSelf_apply_apply, IsSl2Triple.HasPrimitiveVectorWith.lie_h_pow_toEnd_f, baseChangeHom_apply_apply, Matrix.isRepresentation.toEnd_surjective, Matrix.toLinAlgEquiv_self, FiniteField.minpoly_frobeniusAlgHom, Module.AEval'_def, hasEigenvalue_iff_isRoot, AlgEquiv.moduleEndSelfOp_symm_apply, minpoly_algEquiv_toLinearMap, LieAlgebra.IsKilling.cartanEquivDual_apply_apply, LinearMap.toMatrixAlgEquiv'_symm, LieModule.toEnd_eq_zero_iff, Algebra.norm_apply, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, LieAlgebra.isNilpotent_ad_of_mem_rootSpace, Representation.ofModule_asAlgebraHom_apply_apply, isIntegral, AlgebraicGeometry.tilde.isUnit_algebraMap_end_basicOpen, Polynomial.aeval_endomorphism, Matrix.isRepresentation.eq_toEnd_of_represents, LieModule.traceForm_apply_apply, LieAlgebra.IsKilling.isSemisimple_ad_of_mem_isCartanSubalgebra, Algebra.baseChange_lmul, LieModule.trace_toEnd_genWeightSpaceChain_eq_zero, LieModule.maxGenEigenSpace_toEnd_eq_top, AlgEquiv.moduleEndSelf_symm_apply, Matrix.toLinAlgEquiv'_toMatrixAlgEquiv', LinearEquiv.lieConj_symm, LieAlgebra.rank_eq_natTrailingDegree, ker_aeval_ring_hom'_unit_polynomial, Algebra.lmul_isUnit_iff, Module.ker_algebraMap_end, endVecAlgEquivMatrixEnd_symm_apply_apply, Matrix.toLinAlgEquiv'_one, IsSemisimple.minpoly_squarefree, lTensorAlgHom_apply_apply, LieAlgebra.ad_lie, LieModule.isNilpotent_iff_forall', IsLocalizedModule.fromLocalizedModule'_mk, LieSubmodule.coe_toEnd_pow, LinearMap.isIntegral, LieAlgebra.isNilpotent_range_ad_iff, LieModule.mem_genWeightSpaceOf, Matrix.toLinAlgEquiv'_symm, mulSemiringActionToAlgEquiv_conjAct_surjective, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing, IsLocalizedModule.map_units, LieAlgebra.nilpotent_ad_of_nilpotent_algebra, LieModule.instIsFaithfulEnd, Representation.asModuleEquiv_map_smul, LieModule.coe_lcs_range_toEnd_eq, LieModule.toEnd_module_end, LieAlgebra.mem_zeroRootSubalgebra, LinearMap.toMatrixAlgEquiv_apply', mem_spectrum_iff_isRoot_charpoly, LieModule.iterate_toEnd_mem_lowerCentralSeries, Algebra.coe_lmul_eq_mul, LinearEquiv.conjAlgEquiv_surjective, hasEigenvalue_iff_mem_spectrum, LinearMap.not_hasEigenvalue_zero_tfae, LieDerivation.coe_ad_apply_eq_ad_apply, Algebra.trace_apply, Algebra.FormallyUnramified.comp_sec, LieAlgebra.isNilpotent_iff_forall, LieAlgebra.ad_ker_eq_bot_of_hasTrivialRadical, LinearMap.toMatrixAlgEquiv_reindexRange, TensorProduct.AlgebraTensorModule.smul_eq_lsmul_rTensor, LieAlgebra.isNilpotent_ad_of_isNilpotent, LinearMap.toMatrixAlgEquiv_mul, Matrix.minpoly_toLin, Matrix.Represents.algebraMap, LieModule.commute_toEnd_of_mem_center_left, Module.AEval.mem_mapSubmodule_apply, Representation.asAlgebraHom_mem_of_forall_mem, Matrix.toLpLinAlgEquiv_symm_apply, LieAlgebra.ad_ker_eq_self_module_ker, exists_isNilpotent_isSemisimple, HasUnifEigenvalue.mem_spectrum, LinearMap.toMatrixAlgEquiv_transpose_apply, eigenspace_aeval_polynomial_degree_1, Algebra.leftMulMatrix_apply, Matrix.toLinAlgEquiv_toMatrixAlgEquiv, Matrix.toLinAlgEquiv_symm, LinearMap.toMatrixAlgEquiv_transpose_apply', Module.instFinitePolynomialAEval', mem_subalgebraCenter_iff, Algebra.lsmul_coe, LieModule.Weight.hasEigenvalueAt, AlgHom.mulLeftRightMatrix.comp_inv, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, LinearMap.toMatrixAlgEquiv'_comp, LieModule.rank_le_natTrailingDegree_charpoly_ad, LieSubalgebra.coe_ad, LieModule.toEnd_matrix, LieModule.toEnd_pow_comp_lieHom, IsAzumaya.AlgHom.mulLeftRight_bij, Matrix.spectrum_toLin', LieSubalgebra.ad_comp_incl_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_isUnit_inv_apply_eq_iff 📖	mathematical	IsUnit Module.End instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instSemiring RingHom.instFunLike algebraMap instAlgebra	LinearMap.instFunLike RingHom.id Units.val Units Units.instInv IsUnit.unit SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	isUnit_apply_inv_apply_of_isUnit Function.Bijective.injective isUnit_iff LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul
algebraMap_isUnit_inv_apply_eq_iff' 📖	mathematical	IsUnit Module.End instMonoid DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring instSemiring RingHom.instFunLike algebraMap instAlgebra	LinearMap.instFunLike RingHom.id Units.val Units Units.instInv IsUnit.unit SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	isUnit_apply_inv_apply_of_isUnit Function.Bijective.injective isUnit_iff LinearMap.map_smul_of_tower LinearMap.IsScalarTower.compatibleSMul

Module.IsTorsionFree

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_faithfulSMul 📖	mathematical	—	Module.IsTorsionFree NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	Function.Injective.moduleIsTorsionFree FaithfulSMul.algebraMap_injective Algebra.algebraMap_eq_smul_one smul_assoc
to_faithfulSMul 📖	mathematical	—	FaithfulSMul Algebra.toSMul CommRing.toCommSemiring Ring.toSemiring	—	smul_left_injective one_ne_zero NeZero.one
trans_faithfulSMul 📖	mathematical	—	Module.IsTorsionFree CommSemiring.toSemiring	—	comap IsRegular.of_ne_zero IsRegular.ne_zero algebraMap_smul

NeZero

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_faithfulSMul 📖	mathematical	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	nat_of_injective RingHom.instRingHomClass faithfulSMul_iff_injective_smul_one

NoZeroDivisors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
of_faithfulSMul 📖	mathematical	—	NoZeroDivisors Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass	—	Function.Injective.noZeroDivisors FaithfulSMul.algebraMap_injective map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass

NoZeroSMulDivisors

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
iff_algebraMap_injective 📖	mathematical	—	Module.IsTorsionFree CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	Module.isTorsionFree_iff_algebraMap_injective
iff_faithfulSMul 📖	mathematical	—	Module.IsTorsionFree CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring FaithfulSMul Algebra.toSMul	—	Module.isTorsionFree_iff_faithfulSMul

PUnit

Definitions

Name	Category	Theorems
algebra 📖	CompOp	1 math math: Algebra.algebraMap_pUnit

Ring

Definitions

Name	Category	Theorems
toIntAlgebra 📖	CompOp	348 math math: IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime, RootPairing.GeckConstruction.h_def, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow, WittVector.aeval_verschiebung_poly', Differential.implicitDeriv_C, Ideal.absNorm_span_insert, NumberField.isCoprime_differentIdeal_of_isCoprime_discr, Differential.algHom_deriv, IsPrimitiveRoot.totient_le_degree_minpoly, RootPairing.Base.injective_pairingIn, jacobiSum_mem_algebraAdjoin_of_pow_eq_one, one_le_pow_mul_abs_eval_div, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, WittVector.ghostComponent_apply, NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal, NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply', IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow, ChevalleyThm.chevalley_polynomialC, IsPrimitiveRoot.minpoly_dvd_pow_mod, MulChar.apply_mem_algebraAdjoin_of_pow_eq_one, CongruenceSubgroup.exists_Gamma_le_conj', IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow, BoxIntegral.unitPartition.mem_smul_span_iff, RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_right, Real.isIntegral_two_mul_sin_rat_mul_pi, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, FractionalIdeal.absNorm_eq', ModularGroup.one_lt_normSq_T_zpow_smul, CongruenceSubgroup.strictPeriods_Gamma0, Algebra.discr_eq_discr, IsPrimitiveRoot.subOneIntegralPowerBasis_gen, MulChar.apply_mem_algebraAdjoin, Rat.isFractionRingDen, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one', RingOfIntegers.exponent_eq_sInf, RootPairing.Base.pairingIn_le_zero_of_ne, jacobiTheta_T_sq_smul, ModularForm.levelOne_neg_weight_rank_zero, Ideal.absNorm_eq_pow_inertiaDeg', Subgroup.IsArithmetic.is_commensurable, ModularGroup.sl_moeb, IsPrimitiveRoot.is_roots_of_minpoly, NumberField.RingOfIntegers.withValEquiv_symm_apply, IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two, ModularGroup.coe_T_zpow_smul_eq, NumberField.FinitePlace.prod_eq_inv_abs_norm_int, CongruenceSubgroup.exists_Gamma_le_conj, Real.isIntegral_two_mul_cos_rat_mul_pi, Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL, DifferentialAlgebra.deriv_algebraMap, RootPairing.EmbeddedG2.toIsValuedIn, LindemannWeierstrass.exp_polynomial_approx, IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow, RootPairing.pairingIn_pairingIn_mem_set_of_length_eq, RootPairing.zero_le_pairingIn_of_root_sub_mem, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two, ModularGroup.tendsto_abs_re_smul, Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime, IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply, ModularGroup.exists_max_im, RingHom.toIntAlgHom_apply, RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne, Rat.associated_num_den, Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow, CharP.ker_intAlgebraMap_eq_span, instIsGaloisGroupIntRingOfIntegersOfRat, isCusp_SL2Z_iff', RootPairing.pairingIn_pairingIn_mem_set_of_length_eq_of_ne, IsPrimitiveRoot.minpoly_eq_pow_coprime, ModularGroup.im_T_smul, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime, ChevalleyThm.chevalley_mvPolynomialC, RootPairing.pairingIn_eq_zero_of_add_notMem_of_sub_notMem, IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime, Algebra.coe_norm_int, NonUnitalSubring.unitization_apply, CommRingCat.coproductCocone_inl, IsIntegral.ratCast_iff, RootPairing.isG2_iff, WittVector.mulN_coeff, Subgroup.strictWidthInfty_eq_one_of_T_mem, IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply, algebraMap.coe_deriv, RootPairing.IsG2.toIsValuedIn, EisensteinSeries.G2_S_transform, Complex.isIntegral_exp_rat_mul_pi_mul_I, ModularGroup.SL_to_GL_tower, ModularFormClass.one_mem_strictPeriods_SL2Z, Differential.coeff_mapCoeffs, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two, NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors, jacobiTheta_S_smul, ModularForm.levelOne_weight_zero_rank_one, ModularGroup.re_T_smul, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, Algebra.Presentation.coeffs_subset_core, CongruenceSubgroup.strictWidthInfty_Gamma0, IsPrimitiveRoot.integralPowerBasis'_gen, Algebra.Presentation.coeffs_relation_subset_core, Real.isAlgebraic_tan_rat_mul_pi, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two', Complex.isAlgebraic_sin_rat_mul_pi, CommRingCat.coproductCocone_inr, Real.isAlgebraic_cos_rat_mul_pi, IsPrimitiveRoot.subOneIntegralPowerBasis'_gen, Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt, RootPairing.coxeterWeightIn_eq_zero_iff, IsPrimitiveRoot.power_basis_int'_dim, RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_left, Subgroup.IsArithmetic.isFiniteRelIndexSL, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure, RootPairing.IsNotG2.toIsValuedIn, UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero, UpperHalfPlane.modular_S_smul, Subgroup.strictPeriods_eq_zmultiples_one_of_T_mem, ModularGroup.re_T_inv_smul, NumberField.house.exists_ne_zero_int_vec_house_le, CongruenceSubgroup.isArithmetic_conj_SL2Z, EisensteinSeries.q_expansion_riemannZeta, NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm, RingOfIntegers.not_dvd_exponent_iff, mem_subalgebraOfSubring, IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim, ModularGroup.normSq_S_smul_lt_one, RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_right, NumberField.discr_eq_discr, ModularGroup.exists_row_one_eq_and_min_re, IsPrimitiveRoot.minpoly_dvd_expand, WittVector.IsPoly.poly, IsCyclotomicExtension.ring_of_integers', IsPrimitiveRoot.minpoly_dvd_mod_p, Differential.mapCoeffs_monomial, RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed, ModularGroup.re_T_zpow_smul, IsCyclotomicExtension.ringOfIntegers, PadicInt.coe_adicCompletionIntegersEquiv_apply, Ideal.relNorm_int, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one, exists_jacobiSum_eq_neg_one_add, Differential.mapCoeffs_C, RootPairing.chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx, IsCyclotomicExtension.Rat.inertiaDeg_eq, ModularGroup.im_lt_im_S_smul, NumberField.Units.dirichletUnitTheorem.seq_norm_le, IsPrimitiveRoot.separable_minpoly_mod, NumberField.integralBasis_repr_apply, Complex.isIntegral_two_mul_sin_rat_mul_pi, Int.absNorm_under_mem, Polynomial.hermite_eq_deriv_gaussian', IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, Subgroup.isArithmetic_iff_finiteIndex, RootPairing.IsG2.pairingIn_mem_zero_one_three, CommRingCat.coproductCocone_pt, IsPrimitiveRoot.norm_toInteger_sub_one_eq_one, ModularGroup.im_T_zpow_smul, FractionalIdeal.absNorm_eq, EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF, RootPairing.EmbeddedG2.pairingIn_long_short, subalgebraOfSubring_toSubsemiring, IsPrimitiveRoot.isIntegral, NumberField.RingOfIntegers.mk_zero, IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one', isCusp_SL2Z_iff, RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic, Polynomial.deriv_gaussian_eq_hermite_mul_gaussian, RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_left, ModularForm.slash_action_eq'_iff, surjective_cosetToCuspOrbit, Subbimodule.coe_toSubbimoduleInt, CongruenceSubgroup.strictWidthInfty_Gamma1, EisensteinSeries.eisensteinSeries_SIF_apply, IsCyclotomicExtension.Rat.ncard_primesOver_of_prime, IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one, Rat.isFractionRing, NumberField.RingOfIntegers.withValEquiv_apply, RootPairing.forall_pairingIn_eq_swap_or, Complex.isIntegral_exp_neg_rat_mul_pi_mul_I, RootPairing.EmbeddedG2.pairingIn_short_long, ModularGroup.exists_one_half_le_im_smul, Subbimodule.coe_toSubbimoduleNat, Polynomial.hermite_eq_deriv_gaussian, Differential.mapCoeffs_X, WittVector.coeff_frobeniusFun, NumberField.discr_mem_differentIdeal, UpperHalfPlane.petersson_slash_SL, NumberField.absNorm_differentIdeal, NumberField.RingOfIntegers.isIntegral_coe, ModularForm.SL_slash_def, RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff, IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply, NumberField.RingOfIntegers.mk_one, Rat.isFractionRingNum, IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two, Differential.algHom_deriv', CongruenceSubgroup.strictPeriods_Gamma1, RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed', Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, NumberField.RingOfIntegers.instIsIntegralClosureInt, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Int.absNorm_under_dvd_absNorm, Rat.isLocalizationIsInteger_iff, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two, SlashInvariantForm.slash_action_eqn_SL'', CongruenceSubgroup.strictWidthInfty_Gamma, IsPrimitiveRoot.squarefree_minpoly_mod, transcendental_liouvilleNumber, UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip, EisensteinSeries.q_expansion_bernoulli, RootPairing.pairingIn_rat, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd, RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_right, IsPrimitiveRoot.card_quotient_toInteger_sub_one, IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow, ModularGroup.im_smul_eq_div_normSq, IsCyclotomicExtension.Rat.inertiaDegIn_eq, CommRingCat.coproductCoconeIsColimit_desc, witt_structure_prop, RootPairing.pairingIn_le_zero_of_root_add_mem, Real.isAlgebraic_sin_rat_mul_pi, WittVector.coeff_select, RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_left, EisensteinSeries.tendsto_double_sum_S_act, CongruenceSubgroup.strictPeriods_Gamma, cosetToCuspOrbit_apply_mk, Rat.int_algebraMap_injective, NonUnitalSubring.unitization_range, Complex.isIntegral_two_mul_cos_rat_mul_pi, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span, Differential.deriv_aeval_eq, RingOfIntegers.exponent_eq_one_iff, Subgroup.strictPeriods_SL2Z, Differential.logDeriv_eq_zero, IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime, NumberField.RingOfIntegers.isIntegral, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two, RootPairing.chainBotCoeff_if_one_zero, RootPairing.chainTopCoeff_if_one_zero, NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd, Rat.int_algebraMap_surjective, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegersOfPrimePow, ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le, IsPrimitiveRoot.integralPowerBasis_dim, IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd, RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn, FractionalIdeal.abs_det_basis_change, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen, IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd, Ideal.span_singleton_absNorm, SlashInvariantForm.vAdd_width_periodic, ModularGroup.exists_smul_mem_fd, IsCyclotomicExtension.Rat.adjoin_singleton_eq_top, RootPairing.chainTopCoeff_sub_chainBotCoeff, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply, NumberField.RingOfIntegers.instIsIntegralInt, Differential.implicitDeriv_X, RingHom.toIntAlgHom_coe, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, IsPrimitiveRoot.self_sub_one_pow_dvd_order, Ideal.absNorm_eq_pow_inertiaDeg, EisensteinSeries.eisensteinSeriesSIF_apply, IsPrimitiveRoot.coe_toInteger, ModularGroup.im_T_inv_smul, NumberField.Embeddings.finite_of_norm_le, IsPrimitiveRoot.integralPowerBasis_gen, algebraMap_int_eq, IsCyclotomicExtension.Rat.ramificationIdx_eq, UpperHalfPlane.modular_T_zpow_smul, Differential.algEquiv_deriv', IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one, IsPrimitiveRoot.pow_isRoot_minpoly, EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn, RootPairing.isNotG2_iff, Complex.isAlgebraic_tan_rat_mul_pi, instIsLocalizationIntPosRat, Subgroup.IsArithmetic.finiteIndex_comap, ModularForm.SL_slash_apply, IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd, Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange, EisensteinSeries.eisSummand_SL2_apply, WittVector.aeval_verschiebungPoly, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, RootPairing.IsG2.exists_pairingIn_neg_three, IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd, Polynomial.shiftedLegendre_eval_symm, isIntegral_two_mul_cos_rat_mul_pi, IsPrimitiveRoot.minpoly_eq_pow, MvPolynomial.exists_restrict_to_vars, Complex.isAlgebraic_cos_rat_mul_pi, Algebra.coe_trace_int, Int.absNorm_under_eq_sInf, Ideal.absNorm_span_singleton, IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton, RootPairing.EmbeddedG2.pairingIn_shortAddLong_left, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd, IsPrimitiveRoot.minpoly_dvd_cyclotomic, RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic, NumberField.RingOfIntegers.minpoly_coe, IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime, Int.cast_mem_ideal_iff, Liouville.transcendental, RootPairing.GeckConstruction.h_eq_diagonal, Polynomial.cyclotomic_eq_minpoly, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime, EisensteinSeries.eisensteinSeriesSIF_mdifferentiable, RootPairing.EmbeddedG2.pairingIn_shortAddLong_right, WittVector.coeff_frobenius, Subgroup.strictWidthInfty_SL2Z, Ideal.ringChar_quot, IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two', ModularGroup.SL_neg_smul, Int.liesOver_span_absNorm, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime, RingHom.toIntAlgHom_injective, Algebra.Presentation.instFiniteTypeIntCoreOfFinite, Complex.isIntegral_int_I, Algebra.adjoin_int, CommRingCat.coproductCocone_ι, EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act, IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime, Differential.algEquiv_deriv, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one, RootPairing.chainBotCoeff_sub_chainTopCoeff, ModularGroup.exists_eq_T_zpow_of_c_eq_zero, Nat.absNorm_under_prime, UpperHalfPlane.modular_T_smul, Rat.ringOfIntegersWithValEquiv_apply, IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two, ModularGroup.smul_eq_lcRow0_add, SlashInvariantForm.T_zpow_width_invariant, EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF, RootPairing.Base.chainTopCoeff_eq_of_ne, IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one, Ideal.absNorm_dvd_norm_of_mem, RootPairing.baseOf_pairwise_pairing_le_zero, RootPairing.IsNotG2.pairingIn_mem_zero_one_two

RingHom

Definitions

Name	Category	Theorems
commSemiringToCommRing 📖	CompOp	—

Semiring

Definitions

Name	Category	Theorems
toNatAlgebra 📖	CompOp	12 math math: QuadraticMap.canLift, mem_subalgebraOfSubsemiring, NonUnitalSubsemiring.unitization_apply, NNRat.isFractionRing, subalgebraOfSubsemiring_toSubsemiring, Subbimodule.coe_toSubbimoduleInt, Subbimodule.coe_toSubbimoduleNat, QuadraticMap.canLift', RingHom.toNatAlgHom_coe, NonUnitalSubsemiring.unitization_range, RingHom.toNatAlgHom_apply, Algebra.adjoin_nat

ULift

Definitions

Name	Category	Theorems
algebra 📖	CompOp	3 math math: algEquiv_apply, down_algebraMap, algebraMap_eq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_eq 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap algebra	—	—
down_algebraMap 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring semiring RingHom.instFunLike algebraMap algebra	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_comp_intCast 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring RingHom.instFunLike algebraMap AddGroupWithOne.toIntCast Ring.toAddGroupWithOne CommRing.toRing	—	map_intCast RingHom.instRingHomClass
algebraMap_comp_natCast 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	map_natCast RingHom.instRingHomClass
algebraMap_int_eq 📖	mathematical	—	algebraMap Int.instCommSemiring Ring.toSemiring Ring.toIntAlgebra Int.castRingHom Ring.toNonAssocRing	—	—
algebraMap_smul 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	algebra_compatible_smul
algebra_compatible_smul 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring Module.toDistribMulAction DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	one_smul smul_assoc Algebra.smul_def mul_one
bijective_algebraMap_of_linearEquiv 📖	mathematical	—	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	RingHomInvPair.ids bijective_algebraMap_of_linearMap LinearEquiv.bijective
bijective_algebraMap_of_linearMap 📖	mathematical	Function.Bijective DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule LinearMap.instFunLike	RingHom RingHom.instFunLike algebraMap	—	injective_algebraMap_of_linearMap surjective_algebraMap_of_linearMap
faithfulSMul_iff_algebraMap_injective 📖	mathematical	—	FaithfulSMul Algebra.toSMul DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	faithfulSMul_iff_injective_smul_one IsScalarTower.right Algebra.algebraMap_eq_smul_one'
injective_algebraMap_of_linearMap 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule LinearMap.instFunLike	RingHom RingHom.instFunLike algebraMap	—	mul_one smul_eq_mul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass Algebra.smul_def
instFaithfulSMulIntOfCharZero 📖	mathematical	—	FaithfulSMul SubNegMonoid.toZSMul AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne	—	RingHom.injective_int
instFaithfulSMulNatOfCharZero 📖	mathematical	—	FaithfulSMul AddMonoid.toNatSMul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	RingHom.injective_nat
instSMulCommClass 📖	mathematical	—	SMulCommClass Algebra.toSMul	—	Algebra.smul_def mul_smul_comm Algebra.to_smulCommClass
int_algebra_subsingleton 📖	mathematical	—	Algebra Int.instCommSemiring Ring.toSemiring	—	Algebra.algebra_ext RingHom.congr_fun RingHom.Int.subsingleton_ringHom
isSMulRegular_algebraMap_iff 📖	mathematical	—	IsSMulRegular SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	—	Equiv.isSMulRegular_congr algebraMap_smul
nat_algebra_subsingleton 📖	mathematical	—	Algebra Nat.instCommSemiring	—	Algebra.algebra_ext eq_natCast RingHom.instRingHomClass
smul_algebra_smul_comm 📖	mathematical	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction CommSemiring.toSemiring	—	SMulCommClass.smul_comm IsScalarTower.to_smulCommClass'
surjective_algebraMap_of_linearMap 📖	mathematical	DFunLike.coe LinearMap CommSemiring.toSemiring RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule Algebra.toModule LinearMap.instFunLike	RingHom RingHom.instFunLike algebraMap	—	Algebra.algebraMap_eq_smul_one smul_smul mul_one smul_eq_mul map_smul SemilinearMapClass.toMulActionSemiHomClass LinearMap.semilinearMapClass one_mul smul_mul_assoc IsScalarTower.right mul_comm

algebraMap

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_eq_zero_iff 📖	mathematical	—	Algebra.cast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	FaithfulSMul.algebraMap_eq_zero_iff
coe_inj 📖	mathematical	—	Algebra.cast	—	FaithfulSMul.algebraMap_injective
coe_prod 📖	mathematical	—	Algebra.cast CommSemiring.toSemiring Finset.prod CommSemiring.toCommMonoid	—	map_prod MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
coe_sum 📖	mathematical	—	Algebra.cast CommSemiring.toSemiring Finset.sum NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	—	map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass
lift_map_eq_zero_iff 📖	mathematical	—	Algebra.cast MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring	—	coe_eq_zero_iff

---

← Back to Index