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, algebra'	16
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_apply', 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	67
Total	83

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, Module.Finite.instAtPrimeLocalizationAlgebraMapSubmonoidPrimeCompl, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, Module.Finite.instFractionRingLocalizationAlgebraMapSubmonoidNonZeroDivisors, 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, 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	4 math math: JacobsonNoether.exist_pow_eq_zero_of_le, instCharPLinearMapSubtypeMemSubringCenterId, instExpCharLinearMapSubtypeMemSubringCenterId, JacobsonNoether.exists_separable_and_not_isCentral
ofSubring 📖	CompOp	13 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, LocalSubring.instIsScalarTowerSubtypeMemSubringToSubringOfPrime, minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure, algebraMap_ofSubring_apply, Valuation.HasExtension.instIsScalarTowerInteger
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 NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing SetLike.instMembership Subring.instSetLike SubsemiringClass.toCommSemiring CommRing.toCommSemiring SubringClass.toSubsemiringClass Subring.instSubringClass CommSemiring.toSemiring ofSubring CommRing.toRing id Subring.subtype	—	SubringClass.toSubsemiringClass Subring.instSubringClass
algebraMap_ofSubring_apply 📖	mathematical	—	DFunLike.coe RingHom Subring NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing SetLike.instMembership Subring.instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring CommRing.toCommSemiring SubringClass.toSubsemiringClass Subring.instSubringClass RingHom.instFunLike algebraMap ofSubring CommRing.toRing 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 NonAssocCommRing.toNonAssocRing CommRing.toNonAssocCommRing SetLike.instMembership Subring.instSetLike Semiring.toNonAssocSemiring CommSemiring.toSemiring SubsemiringClass.toCommSemiring CommRing.toCommSemiring SubringClass.toSubsemiringClass Subring.instSubringClass RingHom.instFunLike algebraMap ofSubring CommRing.toRing 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.toPow 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 📖	mathematical	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	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring 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	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids EquivLike.toFunLike instEquivLike extendScalarsOfSurjective CommSemiring.toSemiring	—	RingHomInvPair.ids
extendScalarsOfSurjective_symm 📖	mathematical	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap	symm RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids extendScalarsOfSurjective CommSemiring.toSemiring	—	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	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring instFunLike extendScalarsOfSurjective CommSemiring.toSemiring	—	—
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	282 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, LieAlgebra.ad_isSemisimple_of_isSemisimple, 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, LocalizedModule.lift'_mk, 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, algebraMap_isUnit_inv_apply_eq_iff', 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.lie_mem_maxGenEigenspace_toEnd, LieModule.IsTriangularizable.maxGenEigenspace_eq_top, rTensorAlgHom_apply_apply, LieSubmodule.trace_eq_trace_restrict_of_le_idealizer, 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, LieAlgebra.trace_toEnd_eq_zero, 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, isNilpotent_restrict_maxGenEigenspace_sub_algebraMap, 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, LieSubalgebra.isNilpotent_ad_of_isNilpotent_ad, 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, exists_isNilpotent_isSemisimple_of_separable_of_dvd_pow, 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, LocalizedModule.lift_mk, 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, ContinuousLinearMap.spectrum_eq, hasEigenvalue_iff_isRoot, AlgEquiv.moduleEndSelfOp_symm_apply, isNilpotent_restrict_sub_algebraMap, 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, LieAlgebra.commute_ad_of_commute, 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, algebraMap_isUnit_inv_apply_eq_iff, 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	DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Units.val instMonoid Units Units.instInv IsUnit.unit RingHom CommSemiring.toSemiring instSemiring RingHom.instFunLike algebraMap instAlgebra 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	DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring Units.val instMonoid Units Units.instInv IsUnit.unit RingHom CommSemiring.toSemiring instSemiring RingHom.instFunLike algebraMap instAlgebra 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	367 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', OnePoint.isBoundedAt_iff_exists_SL2Z, 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, NumberField.RingOfIntegers.mk_eq_mk, IsCyclotomicExtension.Rat.ramificationIdxIn_eq, Ideal.norm_dvd_iff, 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, OnePoint.isZeroAt_iff_exists_SL2Z, 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, NumberField.RingOfIntegers.coe_mk, 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, NumberField.RingOfIntegers.mk_mul_mk, 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, NumberField.RingOfIntegers.mk_sub_mk, 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, NumberField.RingOfIntegers.mk_add_mk, 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.eq_smul_self_of_mem_fdo_mem_fdo, 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, map_isIntegral_int, RootPairing.IsG2.pairingIn_mem_zero_one_three, CommRingCat.coproductCocone_pt, IsLiouville.isLiouville, 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, Differential.deriv_aeval_eq_implicitDeriv, 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, EisensteinSeries.E_qExpansion_coeff, 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, NumberField.RingOfIntegers.neg_mk, 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, Polynomial.isIntegral_of_mahlerMeasure_eq_one, 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, NumberField.RingOfIntegers.map_mk, ModularForm.SL_slash_apply, IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd, Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange, EisensteinSeries.eisSummand_SL2_apply, RootPairing.RootPositiveForm.rootLength_le_of_pairingIn_eq, WittVector.aeval_verschiebungPoly, EisensteinSeries.eisensteinSeries_SIF_MDifferentiable, RootPairing.IsG2.exists_pairingIn_neg_three, EisensteinSeries.E_qExpansion_coeff_zero, 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.RootPositiveForm.rootLength_lt_of_pairingIn_notMem, 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	7 math math: algEquiv_apply, algEquiv_symm_apply, down_algebraMap, down_algEquiv_symm_apply, AlgHom.down_ulift_apply, AlgHom.ulift_apply, algebraMap_eq
algebra' 📖	CompOp	3 math math: algebraMap_apply', AlgHom.down_ulift_apply, AlgHom.ulift_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_apply' 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring commSemiring RingHom.instFunLike algebraMap algebra'	—	—
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	Function.Bijective DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring 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	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring 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.toNSMul 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	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring 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