Fixed

📁 Source: Mathlib/FieldTheory/Fixed.lean

Statistics

Metric	Count
Definitions fintype, intermediateField, subfield, instAlgebraSubtypeMemSubfieldSubfield, minpoly, subfield, toAlgAutMulEquiv, toAlgHomEquiv, IsInvariantSubfield, toMulSemiringAction	10
Theorems card_le, card_le, intermediateField_mem_iff, subfield_mem_iff, coe_algebraMap, finrank_eq_card, finrank_le_card, instFiniteDimensionalSubtypeMemSubfieldSubfield, instIsInvariantSubfieldSubfield, instSMulCommClassSubtypeMemSubfieldSubfield, isIntegral, isSeparable, linearIndependent_smul_of_linearIndependent, eval₂, eval₂', irreducible, irreducible_aux, monic, ne_one, of_eval₂, minpoly_eq_minpoly, normal, rank_le_card, smul, smulCommClass', smul_polynomial, toAlgAut_bijective, toAlgAut_surjective, toAlgHom_bijective, smul_mem, cardinalMk_algHom, finrank_algHom, instIsInvariantSubringOfIsInvariantSubfield, linearIndependent_toLinearMap	34
Total	44

AlgEquiv

Definitions

Name	Category	Theorems
fintype 📖	CompOp	6 math math: FiniteField.card_algEquiv_extension, card_le, groupCohomology.norm_ofAlgebraAutOnUnits_eq, Algebra.norm_eq_prod_automorphisms, trace_eq_sum_automorphisms, prod_galRestrict_eq_norm

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_le 📖	mathematical	—	Fintype.card AlgEquiv Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring fintype Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule	—	instIsDomain AlgHom.card_le Fintype.ofEquiv_card

AlgHom

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card_le 📖	mathematical	—	Fintype.card AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule	—	Algebra.to_smulCommClass instIsDomain finrank_algHom Module.finrank_linearMap_self Module.Free.of_divisionRing commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing

FixedBy

Definitions

Name	Category	Theorems
intermediateField 📖	CompOp	1 math math: intermediateField_mem_iff
subfield 📖	CompOp	1 math math: subfield_mem_iff

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
intermediateField_mem_iff 📖	mathematical	—	IntermediateField SetLike.instMembership IntermediateField.instSetLike intermediateField SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	—
subfield_mem_iff 📖	mathematical	—	Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	—

FixedPoints

Definitions

Name	Category	Theorems
instAlgebraSubtypeMemSubfieldSubfield 📖	CompOp	10 math math: isSeparable, normal, toAlgAut_surjective, isIntegral, toAlgHom_bijective, IsGaloisGroup.fixedPoints, minpoly_eq_minpoly, toAlgAut_bijective, IsGalois.of_fixed_field, coe_algebraMap
minpoly 📖	CompOp	6 math math: minpoly.monic, minpoly.irreducible, minpoly.eval₂', minpoly_eq_minpoly, minpoly.eval₂, minpoly.of_eval₂
subfield 📖	CompOp	23 math math: instFiniteDimensionalSubtypeMemSubfieldSubfield, finrank_eq_card, minpoly.monic, minpoly.irreducible, isSeparable, minpoly.eval₂', rank_le_card, instSMulCommClassSubtypeMemSubfieldSubfield, normal, finrank_le_card, toAlgAut_surjective, isIntegral, smul_polynomial, toAlgHom_bijective, IsGaloisGroup.fixedPoints, minpoly_eq_minpoly, toAlgAut_bijective, smul, smulCommClass', IsGalois.of_fixed_field, coe_algebraMap, instIsInvariantSubfieldSubfield, minpoly.eval₂
toAlgAutMulEquiv 📖	CompOp	—
toAlgHomEquiv 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_algebraMap 📖	mathematical	—	algebraMap Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAlgebraSubtypeMemSubfieldSubfield Subfield.subtype	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass
finrank_eq_card 📖	mathematical	—	Module.finrank Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring Fintype.card	—	le_antisymm finrank_le_card Algebra.to_smulCommClass SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass instIsDomain instFiniteDimensionalSubtypeMemSubfieldSubfield Finite.of_fintype Fintype.card_le_of_injective instSMulCommClassSubtypeMemSubfieldSubfield MulSemiringAction.toAlgHom_injective finrank_algHom Module.finrank_linearMap_self Module.Free.of_divisionRing commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing
finrank_le_card 📖	mathematical	—	Module.finrank Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring Fintype.card	—	Nat.cast_le Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero Module.finrank_eq_rank commRing_strongRankCondition SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing instFiniteDimensionalSubtypeMemSubfieldSubfield Finite.of_fintype rank_le_card
instFiniteDimensionalSubtypeMemSubfieldSubfield 📖	mathematical	—	FiniteDimensional Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid Subfield.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing Subfield.instModuleSubtypeMem AddCommGroup.toAddCommMonoid Semiring.toModule DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring	—	nonempty_fintype IsNoetherian.iff_fg IsNoetherian.iff_rank_lt_aleph0 LE.le.trans_lt rank_le_card Cardinal.natCast_lt_aleph0
instIsInvariantSubfieldSubfield 📖	mathematical	—	IsInvariantSubfield subfield	—	—
instSMulCommClassSubtypeMemSubfieldSubfield 📖	mathematical	—	SMulCommClass Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring Subfield.instSMulSubtypeMem Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id	—	smul_mul' Subtype.prop
isIntegral 📖	mathematical	—	IsIntegral Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.toField DivisionRing.toRing instAlgebraSubtypeMemSubfieldSubfield	—	nonempty_fintype minpoly.monic minpoly.eval₂
isSeparable 📖	mathematical	—	Algebra.IsSeparable Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.toField DivisionRing.toRing instAlgebraSubtypeMemSubfieldSubfield	—	nonempty_fintype IsSeparable.eq_1 minpoly_eq_minpoly Polynomial.separable_map IsLocalRing.toNontrivial Field.instIsLocalRing minpoly.eq_1 Subfield.toSubring_subtype_eq_subtype Polynomial.map_toSubring Polynomial.separable_prod_X_sub_C_iff MulAction.injective_ofQuotientStabilizer
linearIndependent_smul_of_linearIndependent 📖	mathematical	LinearIndepOn Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring SetLike.coe Finset Finset.instSetLike	DFunLike.coe Function.Embedding Function.instFunLikeEmbedding MulAction.toFun DistribMulAction.toMulAction AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring MulSemiringAction.toDistribMulAction Pi.addCommMonoid Pi.Function.module	—	Finset.coe_empty Finset.induction_on linearIndependent_empty_type Finset.coe_insert linearIndepOn_insert Finset.mem_coe Finsupp.mem_span_image_iff_linearCombination eq_of_sub_eq_zero linearIndependent_iff' Finset.sum_attach Finset.sum_apply Pi.smul_apply sub_smul smul_eq_mul Finset.sum_sub_distrib Pi.zero_apply sub_eq_zero MulAction.toFun_apply mul_inv_cancel_left SemigroupAction.mul_smul smul_mul' Finset.smul_sum Finsupp.linearCombination_apply_of_mem_supported smul_smul Finset.mem_attach Submodule.sum_mem Submodule.smul_mem Submodule.subset_span Set.image_congr Set.image_id' Finset.sum_congr one_smul
minpoly_eq_minpoly 📖	mathematical	—	minpoly minpoly Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.toField DivisionRing.toRing instAlgebraSubtypeMemSubfieldSubfield	—	minpoly.eq_of_irreducible_of_monic IsLocalRing.toNontrivial Field.instIsLocalRing minpoly.irreducible minpoly.eval₂ minpoly.monic
normal 📖	mathematical	—	Normal Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid Subfield.toField instAlgebraSubtypeMemSubfieldSubfield	—	IsIntegral.isAlgebraic SubsemiringClass.nontrivial SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing isIntegral nonempty_fintype minpoly_eq_minpoly minpoly.eq_1 coe_algebraMap Subfield.toSubring_subtype_eq_subtype Polynomial.map_toSubring prodXSubSMul.eq_1 Polynomial.Splits.prod Polynomial.Splits.X_sub_C
rank_le_card 📖	mathematical	—	Cardinal Cardinal.instLE Module.rank Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Subfield.instModuleSubtypeMem Semiring.toModule DivisionRing.toDivisionSemiring Cardinal.instNatCast Fintype.card	—	rank_le Cardinal.mk_coe_finset Cardinal.lift_natCast rank_fun' commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Cardinal.addLeftMono IsOrderedRing.toZeroLEOneClass Cardinal.isOrderedRing Cardinal.instCharZero LinearIndependent.cardinal_lift_le_rank linearIndependent_smul_of_linearIndependent
smul 📖	mathematical	—	Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subfield.instRingSubtypeMem DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField IsInvariantSubfield.toMulSemiringAction instIsInvariantSubfieldSubfield	—	instIsInvariantSubfieldSubfield
smulCommClass' 📖	mathematical	—	SMulCommClass Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield Subfield.instSMulSubtypeMem Algebra.toSMul Semifield.toCommSemiring Field.toSemifield CommSemiring.toSemiring Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	SMulCommClass.symm instSMulCommClassSubtypeMemSubfieldSubfield
smul_polynomial 📖	mathematical	—	Polynomial Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField SMulZeroClass.toSMul Polynomial.instZero Polynomial.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Subfield.instRingSubtypeMem DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction IsInvariantSubfield.toMulSemiringAction instIsInvariantSubfieldSubfield	—	Polynomial.induction_on instIsInvariantSubfieldSubfield Polynomial.smul_C smul smul_add smul_mul' smul_pow' Polynomial.smul_X
toAlgAut_bijective 📖	mathematical	—	Function.Bijective AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAlgebraSubtypeMemSubfieldSubfield DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass AlgEquiv.aut MonoidHom.instFunLike MulSemiringAction.toAlgAut instSMulCommClassSubtypeMemSubfieldSubfield	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass instSMulCommClassSubtypeMemSubfieldSubfield Function.Bijective.injective toAlgHom_bijective DFunLike.ext_iff AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass Function.Bijective.surjective
toAlgAut_surjective 📖	mathematical	—	AlgEquiv Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAlgebraSubtypeMemSubfieldSubfield DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass AlgEquiv.aut MonoidHom.instFunLike MulSemiringAction.toAlgAut instSMulCommClassSubtypeMemSubfieldSubfield	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass instSMulCommClassSubtypeMemSubfieldSubfield MonoidHom.normal_ker Quotient.inductionOn₂' QuotientGroup.eq MonoidHom.mem_ker map_mul MonoidHomClass.toMulHomClass MonoidHom.instMonoidHomClass map_inv inv_mul_eq_one AlgEquiv.ext_iff AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass AlgEquiv.commutes' Function.Bijective.surjective toAlgAut_bijective Subgroup.finite_quotient_of_finiteIndex Subgroup.finiteIndex_ker Subgroup.instFiniteSubtypeMem Finite.algEquiv Finite.algHom Module.Free.of_divisionRing instFiniteDimensionalSubtypeMemSubfieldSubfield instIsDomain QuotientGroup.induction_on
toAlgHom_bijective 📖	mathematical	—	Function.Bijective AlgHom Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike subfield DivInvMonoid.toMonoid Group.toDivInvMonoid SubsemiringClass.toCommSemiring Semifield.toCommSemiring Field.toSemifield SubringClass.toSubsemiringClass DivisionRing.toRing SubfieldClass.toSubringClass Subfield.instSubfieldClass DivisionSemiring.toSemiring Semifield.toDivisionSemiring instAlgebraSubtypeMemSubfieldSubfield MulSemiringAction.toAlgHom instSMulCommClassSubtypeMemSubfieldSubfield	—	nonempty_fintype SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass instSMulCommClassSubtypeMemSubfieldSubfield instIsDomain instFiniteDimensionalSubtypeMemSubfieldSubfield Fintype.bijective_iff_injective_and_card MulSemiringAction.toAlgHom_injective le_antisymm Fintype.card_le_of_injective finrank_eq_card LE.le.trans_eq Algebra.to_smulCommClass finrank_algHom Module.finrank_linearMap_self Module.Free.of_divisionRing commRing_strongRankCondition SubsemiringClass.nontrivial IsLocalRing.toNontrivial Field.instIsLocalRing

FixedPoints.minpoly

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eval₂ 📖	mathematical	—	Polynomial.eval₂ Subring DivisionRing.toRing Field.toDivisionRing SetLike.instMembership Subring.instSetLike Subfield.toSubring FixedPoints.subfield DivInvMonoid.toMonoid Group.toDivInvMonoid Ring.toSemiring Subring.toRing Subring.subtype FixedPoints.minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	prodXSubSMul.eval Polynomial.eval₂_eq_eval_map Polynomial.map_toSubring
eval₂' 📖	mathematical	—	Polynomial.eval₂ Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike FixedPoints.subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Subfield.toDivisionRing Subfield.subtype FixedPoints.minpoly MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	eval₂
irreducible 📖	mathematical	—	Irreducible Polynomial Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike FixedPoints.subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring FixedPoints.minpoly	—	SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass Polynomial.irreducible_of_monic SubsemiringClass.noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain monic ne_one irreducible_aux
irreducible_aux 📖	mathematical	Polynomial.Monic Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike FixedPoints.subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField Polynomial Polynomial.instMul FixedPoints.minpoly	Polynomial.instOne	—	dvd_mul_right dvd_mul_left eval₂ mul_eq_zero IsDomain.to_noZeroDivisors instIsDomain Polynomial.eval₂_mul Polynomial.eq_of_monic_of_associated monic associated_of_dvd_dvd Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd AddMemClass.isCancelAdd NonUnitalSubsemiringClass.toAddSubmonoidClass SubringClass.toSubsemiringClass AddCancelMonoid.toIsCancelAdd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero of_eval₂ mul_right_inj' Polynomial.Monic.ne_zero SubsemiringClass.nontrivial SubfieldClass.toSubringClass Subfield.instSubfieldClass IsLocalRing.toNontrivial Field.instIsLocalRing mul_one mul_left_inj' Polynomial.instIsRightCancelMulZeroOfIsCancelAdd IsCancelMulZero.toIsRightCancelMulZero one_mul
monic 📖	mathematical	—	Polynomial.Monic Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike FixedPoints.subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Subfield.toField FixedPoints.minpoly	—	Polynomial.monic_toSubring prodXSubSMul.monic
ne_one 📖	—	—	—	—	eval₂ one_ne_zero NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.eval₂_one
of_eval₂ 📖	mathematical	Polynomial.eval₂ Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike FixedPoints.subfield DivInvMonoid.toMonoid Group.toDivInvMonoid DivisionSemiring.toSemiring DivisionRing.toDivisionSemiring Subfield.toDivisionRing Subfield.subtype MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	Polynomial Semifield.toDivisionSemiring Field.toSemifield Subfield.toField semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring Polynomial.commRing FixedPoints.minpoly	—	Polynomial.map_dvd_map' eq_1 Subfield.toSubring_subtype_eq_subtype Polynomial.map_toSubring prodXSubSMul.eq_1 Fintype.prod_dvd_of_coprime Polynomial.pairwise_coprime_X_sub_C MulAction.injective_ofQuotientStabilizer QuotientGroup.induction_on Polynomial.dvd_iff_isRoot Polynomial.IsRoot.def Polynomial.eval_smul' instIsInvariantSubringOfIsInvariantSubfield FixedPoints.instIsInvariantSubfieldSubfield MulSemiringActionSemiHomClass.toRingHomClass MulSemiringActionHom.instMulSemiringActionSemiHomClassCoeMonoidHom IsInvariantSubring.coe_subtypeHom' SubringClass.toSubsemiringClass SubfieldClass.toSubringClass Subfield.instSubfieldClass MulSemiringActionHom.coe_polynomial map_smul DistribMulActionSemiHomClass.toMulActionSemiHomClass MulSemiringActionSemiHomClass.toDistribMulActionSemiHomClass FixedPoints.smul_polynomial Polynomial.eval_map smul_zero

IsInvariantSubfield

Definitions

Name	Category	Theorems
toMulSemiringAction 📖	CompOp	2 math math: FixedPoints.smul_polynomial, FixedPoints.smul

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
smul_mem 📖	mathematical	Subfield Field.toDivisionRing SetLike.instMembership Subfield.instSetLike	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MulSemiringAction.toDistribMulAction Ring.toSemiring	—	—

(root)

Definitions

Name	Category	Theorems
IsInvariantSubfield 📖	CompData	1 math math: FixedPoints.instIsInvariantSubfieldSubfield

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
cardinalMk_algHom 📖	mathematical	—	Cardinal Cardinal.instLE AlgHom Semifield.toCommSemiring Field.toSemifield Ring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Cardinal.instNatCast Module.finrank LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule LinearMap.addCommMonoid LinearMap.module Semiring.toModule Algebra.to_smulCommClass	—	LinearIndependent.cardinalMk_le_finrank Algebra.to_smulCommClass commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Finite.linearMap Module.Free.of_divisionRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self linearIndependent_toLinearMap instIsDomain
finrank_algHom 📖	mathematical	—	Fintype.card AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Module.finrank LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Algebra.toModule LinearMap.addCommMonoid LinearMap.module Semiring.toModule Algebra.to_smulCommClass	—	LinearIndependent.fintype_card_le_finrank Algebra.to_smulCommClass commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Finite.linearMap Module.Free.of_divisionRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective FiniteDimensional.finiteDimensional_self Module.Projective.of_free Module.Free.self instIsDomain linearIndependent_toLinearMap
instIsInvariantSubringOfIsInvariantSubfield 📖	mathematical	—	IsInvariantSubring DivisionRing.toRing Field.toDivisionRing Subfield.toSubring	—	IsInvariantSubfield.smul_mem
linearIndependent_toLinearMap 📖	mathematical	—	LinearIndependent AlgHom CommSemiring.toSemiring CommRing.toCommSemiring LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule AlgHom.toLinearMap LinearMap.addCommMonoid LinearMap.module Semiring.toModule Algebra.to_smulCommClass	—	Algebra.to_smulCommClass LinearIndependent.comp linearIndependent_monoidHom MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.ext DFunLike.ext_iff LinearIndependent.of_comp

---

← Back to Index