Basic

📁 Source: Mathlib/FieldTheory/Finite/Basic.lean

Statistics

Metric	Count
Definitions `frobeniusAlgEquiv`, `frobeniusAlgEquivOfAlgebraic`, `frobeniusAlgHom`, `fintypeBot`	4
Theorems `sq_add_sq`, `X_pow_card_pow_sub_X_natDegree_eq`, `X_pow_card_pow_sub_X_ne_zero`, `X_pow_card_sub_X_natDegree_eq`, `X_pow_card_sub_X_ne_zero`, `bijective_frobeniusAlgEquivOfAlgebraic_pow`, `bijective_frobeniusAlgHom_pow`, `card`, `card'`, `card_cast_subgroup_card_ne_zero`, `card_image_polynomial_eval`, `cast_card_eq_zero`, `coe_frobeniusAlgEquivOfAlgebraic`, `coe_frobeniusAlgEquivOfAlgebraic_iterate`, `coe_frobeniusAlgHom`, `even_card_iff_char_two`, `even_card_of_char_two`, `exists_nonsquare`, `exists_root_sum_quadratic`, `expand_card`, `forall_pow_eq_one_iff`, `frobeniusAlgEquivOfAlgebraic_apply`, `frobeniusAlgEquivOfAlgebraic_symm_apply`, `frobeniusAlgEquiv_apply`, `frobeniusAlgEquiv_symm_apply`, `frobeniusAlgHom_apply`, `frobenius_pow`, `instIsCyclicAlgEquivOfFinite`, `isPrimePow_card`, `isSquare_iff`, `isSquare_of_char_two`, `minpoly_frobeniusAlgHom`, `odd_card_of_char_ne_two`, `orderOf_frobeniusAlgEquivOfAlgebraic`, `orderOf_frobeniusAlgHom`, `pow_card`, `pow_card_pow`, `pow_card_sub_one_eq_one`, `pow_dichotomy`, `prod_univ_units_id_eq_neg_one`, `roots_X_pow_card_sub_X`, `sum_pow_lt_card_sub_one`, `sum_pow_units`, `sum_subgroup_pow_eq_zero`, `sum_subgroup_units`, `sum_subgroup_units_eq_zero`, `unit_isSquare_iff`, `pow_card_sub_one_eq_one`, `pow_eq_pow`, `pow_prime_eq_self`, `prime_dvd_pow_self_sub`, `prime_dvd_pow_sub_one`, `pow_card_sub_one_eq_one`, `pow_totient`, `pow_card_sub_one_sub_one_mod_card`, `sq_add_sq_modEq`, `sq_add_sq_zmodEq`, `card_bot`, `mem_bot_iff_pow_eq_self`, `roots_X_pow_char_sub_X_bot`, `splits_bot`, `card_units`, `eq_one_or_isUnit_sub_one`, `expand_card`, `fieldRange_castHom_eq_bot`, `frobenius_zmod`, `instSubsingletonSubfield`, `orderOf_dvd_card_sub_one`, `orderOf_units_dvd_card_sub_one`, `pow_card`, `pow_card_pow`, `pow_card_sub_one`, `pow_card_sub_one_eq_one`, `pow_totient`, `sq_add_sq`, `units_pow_card_sub_one_eq_one`, `instFiniteZModUnits`, `mem_bot_iff_intCast`, `pow_pow_modEq_one`	79
Total	83

CharP

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`sq_add_sq` 📖	mathematical	—	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `AddGroupWithOne.toIntCast`	—	`char_is_prime_of_pos` `IsDomain.to_noZeroDivisors` `IsDomain.toNontrivial` `ZMod.sq_add_sq` `ZMod.natCast_val` `dvd_rfl` `ZMod.cast_add` `ZMod.cast_pow` `map_intCast` `RingHom.instRingHomClass`

FiniteField

Definitions

Name	Category	Theorems
`frobeniusAlgEquiv` 📖	CompOp	2 math math: `frobeniusAlgEquiv_symm_apply`, `frobeniusAlgEquiv_apply`
`frobeniusAlgEquivOfAlgebraic` 📖	CompOp	6 math math: `frobeniusAlgEquivOfAlgebraic_apply`, `orderOf_frobeniusAlgEquivOfAlgebraic`, `coe_frobeniusAlgEquivOfAlgebraic`, `frobeniusAlgEquivOfAlgebraic_symm_apply`, `coe_frobeniusAlgEquivOfAlgebraic_iterate`, `bijective_frobeniusAlgEquivOfAlgebraic_pow`
`frobeniusAlgHom` 📖	CompOp	7 math math: `frobeniusAlgHom_apply`, `frobeniusAlgEquiv_symm_apply`, `frobeniusAlgEquivOfAlgebraic_symm_apply`, `minpoly_frobeniusAlgHom`, `bijective_frobeniusAlgHom_pow`, `orderOf_frobeniusAlgHom`, `coe_frobeniusAlgHom`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`X_pow_card_pow_sub_X_natDegree_eq` 📖	mathematical	—	`Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Nat.instMonoid`	—	`X_pow_card_sub_X_natDegree_eq`
`X_pow_card_pow_sub_X_ne_zero` 📖	—	—	—	—	`X_pow_card_sub_X_ne_zero`
`X_pow_card_sub_X_natDegree_eq` 📖	mathematical	—	`Polynomial.natDegree` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Polynomial` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X`	—	`Polynomial.degree_X_pow` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Polynomial.degree_X` `Nat.cast_one` `WithBot.addLeftMono` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `WithBot.zeroLEOneClass` `Nat.instZeroLEOneClass` `WithBot.charZero` `Nat.instCharZero` `Polynomial.natDegree_eq_of_degree_eq` `Polynomial.degree_sub_eq_left_of_degree_lt` `Polynomial.natDegree_X_pow`
`X_pow_card_sub_X_ne_zero` 📖	—	—	—	—	`Polynomial.ne_zero_of_natDegree_gt` `X_pow_card_sub_X_natDegree_eq`
`bijective_frobeniusAlgEquivOfAlgebraic_pow` 📖	mathematical	—	`Function.Bijective` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `AlgEquiv` `Monoid.toNatPow` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `frobeniusAlgEquivOfAlgebraic` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `DivisionRing.toRing` `Field.toDivisionRing` `Module.IsNoetherian.finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Ring.toSemiring` `isNoetherian_of_isNoetherianRing_of_finite` `Ring.toAddCommGroup` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `AddCommGroup.toAddCommMonoid` `isNoetherian_of_finite`	—	`instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.IsNoetherian.finite` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `isNoetherian_of_finite` `Function.Bijective.of_comp_iff'` `MulEquiv.bijective` `map_pow` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `bijective_frobeniusAlgHom_pow`
`bijective_frobeniusAlgHom_pow` 📖	mathematical	—	`Function.Bijective` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Semifield.toCommSemiring` `AlgHom` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Monoid.toNatPow` `AlgHom.End` `frobeniusAlgHom`	—	`orderOf_frobeniusAlgHom` `orderOf_pos_iff` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.IsNoetherian.finite` `isNoetherian_of_finite` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `Function.Injective.bijective_of_nat_card_le` `Finite.algHom` `Module.Free.of_divisionRing` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `Subtype.val_injective` `Equiv.injective` `LE.le.trans_eq` `card_algHom_le_finrank` `Nat.card_eq_fintype_card` `Fintype.card_fin`
`card` 📖	mathematical	—	`Nat.Prime` `Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `PNat.val`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `CharP.char_is_prime` `IsDomain.to_noZeroDivisors` `instIsDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Finite.of_fintype` `VectorSpace.card_fintype` `dvd_rfl` `Fintype.card_le_one_iff` `le_of_eq` `pow_zero` `zero_ne_one` `NeZero.one` `ZMod.card` `Fact.out`
`card'` 📖	mathematical	—	`CharP` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Nat.Prime` `Fintype.card` `Monoid.toNatPow` `Nat.instMonoid` `PNat.val`	—	`CharP.exists` `card`
`card_cast_subgroup_card_ne_zero` 📖	—	—	—	—	`CharP.exists` `CharP.cast_eq_zero_iff` `CharP.char_is_prime_or_zero` `exists_prime_orderOf_dvd_card` `orderOf_units` `Subgroup.orderOf_coe` `sub_self` `eq_zero_of_pow_eq_zero` `isReduced_of_noZeroDivisors` `sub_pow_char_of_commute` `Commute.one_right` `one_pow` `pow_orderOf_eq_one` `LT.lt.ne` `Nat.Prime.one_lt` `orderOf_one` `LT.lt.ne'` `Fintype.card_pos` `One.instNonempty`
`card_image_polynomial_eval` 📖	mathematical	`WithBot` `Preorder.toLT` `WithBot.instPreorder` `Nat.instPreorder` `WithBot.zero` `MulZeroClass.toZero` `Nat.instMulZeroClass` `Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring`	`Fintype.card` `Polynomial.natDegree` `Finset.card` `Finset.image` `Polynomial.eval` `Finset.univ`	—	`Finset.card_le_mul_card_image` `Finset.filter.congr_simp` `Polynomial.mem_roots_sub_C` `Polynomial.eval_sub` `Polynomial.eval_C` `Multiset.toFinset_card_le` `Polynomial.card_roots_sub_C'`
`cast_card_eq_zero` 📖	mathematical	—	`AddMonoidWithOne.toNatCast` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `Fintype.card` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Nat.cast_card_eq_zero`
`coe_frobeniusAlgEquivOfAlgebraic` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike` `frobeniusAlgEquivOfAlgebraic` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card`	—	—
`coe_frobeniusAlgEquivOfAlgebraic_iterate` 📖	mathematical	—	`Nat.iterate` `DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike` `frobeniusAlgEquivOfAlgebraic` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Nat.instMonoid` `Fintype.card`	—	`pow_iterate`
`coe_frobeniusAlgHom` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AlgHom.funLike` `frobeniusAlgHom` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Fintype.card`	—	—
`even_card_iff_char_two` 📖	mathematical	—	`ringChar` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Fintype.card`	—	`card` `ringChar.charP` `Nat.even_iff` `Nat.even_pow` `Nat.Prime.even_iff`
`even_card_of_char_two` 📖	mathematical	`ringChar` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`Fintype.card`	—	`even_card_iff_char_two`
`exists_nonsquare` 📖	mathematical	—	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`Ring.neg_one_ne_one_of_char_ne_two` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `mul_neg` `mul_one` `neg_neg`
`exists_root_sum_quadratic` 📖	mathematical	`Polynomial.degree` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `WithBot` `instOfNatAtLeastTwo` `AddMonoidWithOne.toNatCast` `WithBot.addMonoidWithOne` `Nat.instAddMonoidWithOne` `Nat.instAtLeastTwoHAddOfNat` `Fintype.card`	`Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Polynomial.eval` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Nat.instAtLeastTwoHAddOfNat` `lt_irrefl` `Finset.card_le_univ` `two_mul` `add_lt_add_of_lt_of_le` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `IsRightCancelAdd.addRightStrictMono_of_addRightMono` `AddRightCancelSemigroup.toIsRightCancelAdd` `covariant_swap_add_of_covariant_add` `lt_of_le_of_ne` `card_image_polynomial_eval` `Polynomial.natDegree_eq_of_degree_eq_some` `Polynomial.degree_neg` `Finset.card_union_of_disjoint` `Polynomial.natDegree_neg` `Polynomial.eval_neg` `mul_add` `Distrib.leftDistribClass` `Mathlib.Tactic.Push.not_forall_eq` `neg_add_cancel`
`expand_card` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.expand` `Fintype.card` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`CharP.exists` `card` `expChar_prime` `Polynomial.map_iterateFrobenius_expand` `iterateFrobenius_eq_pow` `frobenius_pow` `RingHom.one_def` `Polynomial.map_id`
`forall_pow_eq_one_iff` 📖	mathematical	—	`Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Monoid.toNatPow` `Units.instMonoid` `Units.instOne` `Fintype.card`	—	`IsCyclic.exists_generator` `instIsCyclicUnitsOfFinite` `instIsDomain` `instFiniteUnits` `Finite.of_fintype` `Nat.card_eq_fintype_card` `Nat.card_units` `orderOf_eq_card_of_forall_mem_zpowers` `orderOf_dvd_iff_pow_eq_one` `pow_mul` `mul_comm` `one_pow`
`frobeniusAlgEquivOfAlgebraic_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike` `frobeniusAlgEquivOfAlgebraic` `Monoid.toNatPow` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Fintype.card`	—	—
`frobeniusAlgEquivOfAlgebraic_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `AlgEquiv.instFunLike` `AlgEquiv.symm` `frobeniusAlgEquivOfAlgebraic` `Function.surjInv` `AlgHom` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AlgHom.funLike` `frobeniusAlgHom` `Function.Bijective.surjective` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHomClass.toRingHom` `Algebra.IsAlgebraic.algHom_bijective`	—	—
`frobeniusAlgEquiv_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AlgEquiv.instFunLike` `frobeniusAlgEquiv` `Monoid.toNatPow` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Fintype.card`	—	—
`frobeniusAlgEquiv_symm_apply` 📖	mathematical	—	`DFunLike.coe` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AlgEquiv.instFunLike` `AlgEquiv.symm` `frobeniusAlgEquiv` `Function.surjInv` `AlgHom` `AlgHom.funLike` `frobeniusAlgHom` `Function.Bijective.surjective` `RingHom` `Semiring.toNonAssocSemiring` `RingHom.instFunLike` `RingHomClass.toRingHom`	—	—
`frobeniusAlgHom_apply` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `AlgHom.funLike` `frobeniusAlgHom` `Monoid.toNatPow` `CommMonoid.toMonoid` `CommRing.toCommMonoid` `Fintype.card`	—	—
`frobenius_pow` 📖	mathematical	`Fintype.card` `Monoid.toNatPow` `Nat.instMonoid`	`RingHom` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.instMonoid` `frobenius` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `RingHom.instOne`	—	`RingHom.ext` `expChar_prime` `RingHom.one_def` `RingHom.id_apply` `pow_card` `pow_zero` `pow_one` `pow_succ'` `pow_succ` `pow_mul` `RingHom.mul_def` `RingHom.comp_apply` `frobenius_def`
`instIsCyclicAlgEquivOfFinite` 📖	mathematical	—	`IsCyclic` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DivInvMonoid.toZPow` `Group.toDivInvMonoid` `AlgEquiv.aut`	—	`Finite.of_injective` `RingHom.injective` `DivisionRing.isSimpleRing` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Algebra.IsAlgebraic.of_finite` `Module.IsNoetherian.finite` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `isNoetherian_of_finite` `bijective_frobeniusAlgEquivOfAlgebraic_pow`
`isPrimePow_card` 📖	mathematical	—	`IsPrimePow` `Nat.instCommMonoidWithZero` `Fintype.card`	—	`card'` `Nat.prime_iff` `Subtype.prop`
`isSquare_iff` 📖	mathematical	—	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Fintype.card` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`MulZeroClass.mul_zero` `unit_isSquare_iff`
`isSquare_of_char_two` 📖	mathematical	`ringChar` `Semiring.toNonAssocSemiring` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	`IsSquare` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain`	—	`ringChar.of_eq` `isSquare_of_charTwo'` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain`
`minpoly_frobeniusAlgHom` 📖	mathematical	—	`minpoly` `LinearMap` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `RingHom.id` `Semiring.toNonAssocSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonAssocSemiring.toNonUnitalNonAssocSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Algebra.toModule` `Module.End.instRing` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `Module.End.instAlgebra` `smulCommClass_self` `CommRing.toCommMonoid` `DistribMulAction.toMulAction` `CommMonoid.toMonoid` `AddCommMonoid.toAddMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Module.toDistribMulAction` `Ring.toSemiring` `CommRing.toRing` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Algebra.toSMul` `Algebra.id` `IsScalarTower.left` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `AlgHom.toLinearMap` `frobeniusAlgHom` `Polynomial` `Polynomial.instSub` `Monoid.toNatPow` `Polynomial.semiring` `Polynomial.X` `Module.finrank` `Polynomial.instOne`	—	`minpoly.eq_of_linearIndependent` `smulCommClass_self` `IsScalarTower.left` `Polynomial.leadingCoeff_X_pow_sub_one` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.IsNoetherian.finite` `isNoetherian_of_finite` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `LinearMap.ext` `Polynomial.aeval_sub` `map_pow` `MonoidWithZeroHomClass.toMonoidHomClass` `RingHomClass.toMonoidWithZeroHomClass` `AlgHomClass.toRingHomClass` `AlgHom.algHomClass` `Polynomial.aeval_X` `map_one` `MonoidHomClass.toOneHomClass` `Module.End.coe_pow` `orderOf_frobeniusAlgHom` `AlgHom.coe_pow` `pow_orderOf_eq_one` `Polynomial.degree_X_pow_sub_C` `MonoidHom.instMonoidHomClass` `LinearIndependent.comp` `LinearIndependent.restrict_scalars'` `Algebra.to_smulCommClass` `LinearMap.instIsScalarTower` `IsScalarTower.right` `Module.Free.instFaithfulSMulOfNontrivial` `Module.Free.of_divisionRing` `linearIndependent_algHom_toLinearMap` `bijective_frobeniusAlgHom_pow`
`odd_card_of_char_ne_two` 📖	mathematical	—	`Fintype.card`	—	`even_card_iff_char_two`
`orderOf_frobeniusAlgEquivOfAlgebraic` 📖	mathematical	—	`orderOf` `AlgEquiv` `Semifield.toCommSemiring` `Field.toSemifield` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `AlgEquiv.aut` `frobeniusAlgEquivOfAlgebraic` `Algebra.IsAlgebraic.of_finite` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `DivisionRing.toRing` `Field.toDivisionRing` `Module.IsNoetherian.finite` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Algebra.toModule` `Ring.toSemiring` `isNoetherian_of_isNoetherianRing_of_finite` `Ring.toAddCommGroup` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `AddCommGroup.toAddCommMonoid` `isNoetherian_of_finite` `Module.finrank` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing`	—	`Algebra.IsAlgebraic.of_finite` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.IsNoetherian.finite` `isNoetherian_of_isNoetherianRing_of_finite` `PrincipalIdealRing.isNoetherianRing` `EuclideanDomain.to_principal_ideal_domain` `isNoetherian_of_finite` `orderOf_eq_iff` `Module.finrank_pos` `commRing_strongRankCondition` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `AlgEquiv.coe_pow` `AlgHom.coe_pow` `orderOf_frobeniusAlgHom`
`orderOf_frobeniusAlgHom` 📖	mathematical	—	`orderOf` `AlgHom` `Semifield.toCommSemiring` `Field.toSemifield` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `AlgHom.End` `frobeniusAlgHom` `Module.finrank` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Algebra.toModule`	—	`orderOf_eq_iff` `Module.finrank_pos` `commRing_strongRankCondition` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Module.IsNoetherian.finite` `isNoetherian_of_finite` `instIsDomain` `instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors` `GroupWithZero.toNoZeroSMulDivisors` `DFunLike.ext` `AlgHom.coe_pow` `pow_iterate` `pow_card` `Polynomial.card_le_degree_of_subset_roots` `Polynomial.eval_sub` `Polynomial.eval_pow` `Polynomial.eval_X` `DFunLike.congr_fun` `Polynomial.coeff_sub` `Polynomial.coeff_X_pow` `LT.lt.ne` `LT.lt.ne'` `Fintype.one_lt_card` `Polynomial.coeff_X_one` `zero_sub` `NeZero.one` `sub_eq_zero` `AlgHom.one_apply` `coe_frobeniusAlgHom` `LE.le.not_gt` `LE.le.trans_lt` `LE.le.trans_eq` `Polynomial.natDegree_sub_le` `Polynomial.natDegree_pow` `IsDomain.to_noZeroDivisors` `Polynomial.natDegree_X` `mul_one` `sup_of_le_left` `Fintype.card_pos` `Nontrivial.to_nonempty` `LT.lt.trans_eq` `Module.card_eq_pow_finrank`
`pow_card` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `Fintype.card`	—	`zero_pow` `Fintype.card_ne_zero` `Nontrivial.to_nonempty` `GroupWithZero.toNontrivial` `Fintype.card_pos` `pow_succ` `pow_card_sub_one_eq_one` `one_mul`
`pow_card_pow` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `Nat.instMonoid` `Fintype.card`	—	`pow_zero` `pow_one` `pow_succ` `pow_mul` `pow_card`
`pow_card_sub_one_eq_one` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `GroupWithZero.toMonoidWithZero` `Fintype.card` `InvOneClass.toOne` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `GroupWithZero.toDivisionMonoid`	—	`Units.val_pow_eq_pow_val` `Units.val_mk0` `Fintype.card_units` `pow_card_eq_one`
`pow_dichotomy` 📖	mathematical	—	`Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Fintype.card` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup`	—	`pow_card_sub_one_eq_one` `mul_self_eq_one_iff` `IsDomain.to_noZeroDivisors` `instIsDomain` `pow_two` `pow_mul` `mul_comm` `Nat.two_mul_odd_div_two` `odd_card_of_char_ne_two`
`prod_univ_units_id_eq_neg_one` 📖	mathematical	—	`Finset.prod` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `CommGroup.toCommMonoid` `Units.instCommGroupUnits` `CommRing.toCommMonoid` `Finset.univ` `Units.instNeg` `NonUnitalNonAssocRing.toHasDistribNeg` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Units.instOne`	—	`Finset.prod_involution` `mul_inv_cancel` `IsDomain.to_noZeroDivisors` `inv_eq_iff_eq_inv` `inv_neg` `inv_one` `inv_inv` `Finset.insert_erase` `Finset.mem_univ` `Finset.prod_insert` `Finset.notMem_erase` `mul_one`
`roots_X_pow_card_sub_X` 📖	mathematical	—	`Polynomial.roots` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `instIsDomain` `Field.toSemifield` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.instSub` `DivisionRing.toRing` `Field.toDivisionRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Fintype.card` `Finset.val` `Finset.univ`	—	`X_pow_card_sub_X_ne_zero` `Fintype.one_lt_card` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `instIsDomain` `Finset.eq_univ_iff_forall` `Multiset.mem_toFinset` `Polynomial.mem_roots` `Polynomial.IsRoot.def` `Polynomial.eval_sub` `Polynomial.eval_pow` `Polynomial.eval_X` `sub_eq_zero` `pow_card` `Multiset.toFinset_val` `Multiset.dedup_eq_self` `Polynomial.nodup_roots` `Polynomial.separable_def` `Polynomial.derivative_sub` `Polynomial.derivative_X` `Polynomial.derivative_X_pow` `Nat.cast_card_eq_zero` `Polynomial.C_0` `MulZeroClass.zero_mul` `zero_sub` `IsCoprime.neg_right` `isCoprime_one_right`
`sum_pow_lt_card_sub_one` 📖	mathematical	`Fintype.card`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Finset.sum_congr` `pow_zero` `Finset.sum_const` `nsmul_one` `cast_card_eq_zero` `Mathlib.Tactic.Contrapose.contrapose₃` `Units.val_injective` `Finset.ext` `isUnit_iff_ne_zero` `Finset.sum_sdiff` `Finset.subset_univ` `Finset.sum_singleton` `zero_pow` `add_zero` `Finset.sum_map` `sum_pow_units`
`sum_pow_units` 📖	mathematical	—	`Finset.sum` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `Finset.univ` `instFintypeUnitsOfDecidableEq` `Monoid.toNatPow` `Units.val` `Fintype.card` `NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `Ring.toAddCommGroup` `DivisionRing.toRing` `Field.toDivisionRing` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`one_pow` `mul_pow` `sum_hom_units` `instIsDomain` `forall_pow_eq_one_iff` `DFunLike.ext_iff` `Fintype.card_units` `Nat.cast_sub` `Fintype.card_pos_iff` `cast_card_eq_zero` `Nat.cast_one` `zero_sub` `Nat.cast_zero`
`sum_subgroup_pow_eq_zero` 📖	mathematical	`Fintype.card` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike`	`Finset.sum` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `Finset.univ` `Monoid.toNatPow` `Units.val` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim` `Unique.instSubsingleton` `NoZeroDivisors.to_isDomain` `exists_pow_ne_one_of_isCyclic` `subgroup_units_cyclic` `Finite.of_fintype` `Nat.card_eq_fintype_card` `Finset.sum_eq_multiset_sum` `Multiset.map_congr` `Multiset.map_map` `Multiset.map_univ_val_equiv` `sub_mul` `mul_comm` `Multiset.sum_map_mul_right` `one_mul` `sub_self` `mul_eq_zero` `Units.ext` `sub_eq_zero`
`sum_subgroup_units` 📖	mathematical	—	`Finset.sum` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.univ` `Units.val` `Bot.bot` `Subgroup.instBot` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`SubmonoidClass.toOneMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `Finset.sum_congr` `Finset.univ_unique` `Finset.sum_singleton` `Set.default_coe_singleton` `sum_subgroup_units_eq_zero`
`sum_subgroup_units_eq_zero` 📖	mathematical	—	`Finset.sum` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring` `Subgroup` `Units.instGroup` `SetLike.instMembership` `Subgroup.instSetLike` `NonUnitalNonAssocSemiring.toAddCommMonoid` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing` `Ring.toNonAssocRing` `Finset.univ` `Units.val` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass`	—	`Subgroup.ne_bot_iff_exists_ne_one` `MulMemClass.isLeftCancelMul` `SubmonoidClass.toMulMemClass` `SubgroupClass.toSubmonoidClass` `Subgroup.instSubgroupClass` `LeftCancelSemigroup.toIsLeftCancelMul` `Finset.univ_map_embedding` `Finset.sum_map` `mul_eq_zero` `sub_mul` `Finset.sum_congr` `one_mul` `sub_self` `Mathlib.Tactic.Contrapose.contrapose₄` `Units.ext` `sub_eq_zero`
`unit_isSquare_iff` 📖	mathematical	—	`IsSquare` `Units` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `Units.instMul` `Monoid.toNatPow` `Units.instMonoid` `Fintype.card` `Units.instOne`	—	`IsCyclic.exists_generator` `instIsCyclicUnitsOfFinite` `instIsDomain` `instFiniteUnits` `Finite.of_fintype` `mem_powers_iff_mem_zpowers` `Nat.two_mul_odd_div_two` `odd_card_of_char_ne_two` `pow_two` `pow_mul` `Units.val_injective` `pow_card_sub_one_eq_one` `Units.ne_zero` `IsLocalRing.toNontrivial` `Field.instIsLocalRing` `Nat.card_eq_fintype_card` `Nat.card_units` `orderOf_eq_card_of_forall_mem_zpowers` `orderOf_dvd_of_pow_eq_one` `Finite.one_lt_card` `Nat.instAtLeastTwoHAddOfNat` `IsStrictOrderedRing.toIsOrderedRing` `Nat.instIsStrictOrderedRing` `Nat.instNontrivial` `mul_comm`

Int

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`prime_dvd_pow_self_sub` 📖	mathematical	`Nat.Prime`	`Monoid.toNatPow` `instMonoid`	—	`ModEq.dvd` `ModEq.symm` `ModEq.pow_prime_eq_self`
`prime_dvd_pow_sub_one` 📖	mathematical	`Nat.Prime` `IsCoprime` `instCommSemiring`	`Monoid.toNatPow` `instMonoid`	—	`ModEq.dvd` `ModEq.symm` `ModEq.pow_card_sub_one_eq_one`

Int.ModEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_card_sub_one_eq_one` 📖	mathematical	`Nat.Prime` `IsCoprime` `Int.instCommSemiring`	`Int.ModEq` `Monoid.toNatPow` `Int.instMonoid`	—	`CharP.intCast_eq_zero_iff` `ZMod.charP` `Prime.coprime_iff_not_dvd` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `Int.instIsDomain` `Nat.prime_iff_prime_int` `IsCoprime.symm` `Int.cast_pow` `Int.cast_one` `ZMod.pow_card_sub_one_eq_one`
`pow_eq_pow` 📖	mathematical	`Nat.Prime`	`Int.ModEq` `Monoid.toNatPow` `Int.instMonoid`	—	`Mathlib.Tactic.GCongr.rel_imp_rel` `instIsTrans` `pow` `symm` `zero_pow` `LT.lt.ne'` `LT.lt.trans_le` `refl` `pow_sub_mul_pow` `pow_mul` `mul` `pow_card_sub_one_eq_one` `IsCoprime.symm` `Prime.coprime_iff_not_dvd` `IsBezout.of_isPrincipalIdealRing` `EuclideanDomain.to_principal_ideal_domain` `Int.instIsDomain` `Nat.prime_iff_prime_int` `Int.modEq_zero_iff_dvd` `one_pow` `one_mul`
`pow_prime_eq_self` 📖	mathematical	`Nat.Prime`	`Int.ModEq` `Monoid.toNatPow` `Int.instMonoid`	—	`Int.cast_pow` `ZMod.pow_card`

Nat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_card_sub_one_sub_one_mod_card` 📖	mathematical	`Prime`	`Monoid.toNatPow` `instMonoid`	—	`ModEq.pow_card_sub_one_eq_one`
`sq_add_sq_modEq` 📖	mathematical	—	`ModEq` `Monoid.toNatPow` `instMonoid`	—	`sq_add_sq_zmodEq`
`sq_add_sq_zmodEq` 📖	mathematical	—	`Int.ModEq` `Monoid.toNatPow` `Int.instMonoid`	—	`ZMod.sq_add_sq` `ZMod.natAbs_valMinAbs_le` `NeZero.of_gt'` `instCanonicallyOrderedAdd` `Prime.one_lt'` `Int.natCast_natAbs` `sq_abs` `ZMod.intCast_eq_intCast_iff` `Int.cast_add` `Int.cast_pow` `ZMod.coe_valMinAbs`

Nat.ModEq

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`pow_card_sub_one_eq_one` 📖	mathematical	`Nat.Prime`	`Nat.ModEq` `Monoid.toNatPow` `Nat.instMonoid`	—	`Int.natCast_modEq_iff` `Nat.cast_pow` `Nat.cast_one` `Int.ModEq.pow_card_sub_one_eq_one` `Nat.isCoprime_iff_coprime`
`pow_totient` 📖	mathematical	—	`Nat.ModEq` `Monoid.toNatPow` `Nat.instMonoid` `Nat.totient`	—	`ZMod.natCast_eq_natCast_iff` `ZMod.pow_totient` `Nat.cast_pow` `Nat.cast_one`

Subfield

Definitions

Name	Category	Theorems
`fintypeBot` 📖	CompOp	1 math math: `roots_X_pow_char_sub_X_bot`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_bot` 📖	mathematical	—	`Nat.card` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`dvd_rfl` `ZMod.fieldRange_castHom_eq_bot` `Nat.card_eq_of_bijective` `RingHom.rangeRestrictField_bijective` `Nat.card_zmod`
`mem_bot_iff_pow_eq_self` 📖	mathematical	—	`Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield`	—	`instIsDomain` `Multiset.mem_map` `Polynomial.Splits.roots_map` `DivisionRing.isSimpleRing` `splits_bot` `roots_X_pow_char_sub_X_bot` `Polynomial.roots.congr_simp` `Polynomial.map_sub` `Polynomial.map_pow` `Polynomial.map_X` `FiniteField.X_pow_card_sub_X_ne_zero` `Nat.Prime.one_lt` `Fact.out` `Polynomial.eval_sub` `Polynomial.eval_pow` `Polynomial.eval_X`
`roots_X_pow_char_sub_X_bot` 📖	mathematical	—	`Polynomial.roots` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `EuclideanDomain.toCommRing` `Field.toEuclideanDomain` `toField` `instIsDomain` `Field.toSemifield` `Polynomial` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Polynomial.instSub` `instRingSubtypeMem` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X` `Finset.val` `Finset.univ` `fintypeBot`	—	`instIsDomain` `card_bot` `Fintype.card_eq_nat_card` `FiniteField.roots_X_pow_card_sub_X`
`splits_bot` 📖	mathematical	—	`Polynomial.Splits` `Subfield` `Field.toDivisionRing` `SetLike.instMembership` `instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `toField` `Polynomial` `Polynomial.instSub` `instRingSubtypeMem` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Polynomial.semiring` `Polynomial.X`	—	`instIsDomain` `Polynomial.splits_iff_card_roots` `roots_X_pow_char_sub_X_bot` `Finset.card_def` `Finset.card_univ` `FiniteField.X_pow_card_sub_X_natDegree_eq` `Nat.Prime.one_lt` `Fact.out` `Fintype.card_eq_nat_card` `card_bot`

ZMod

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`card_units` 📖	mathematical	—	`Fintype.card` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `instFintypeUnitsOfDecidableEq` `fintype` `NeZero.of_gt'` `AddMonoid.toAddZeroClass` `Nat.instAddMonoid` `Nat.instPreorder` `Nat.instCanonicallyOrderedAdd` `Nat.instOne` `Nat.Prime.one_lt'` `decidableEq`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Fintype.card_units` `card`
`eq_one_or_isUnit_sub_one` 📖	mathematical	`Monoid.toNatPow` `Nat.instMonoid` `orderOf` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing`	`AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `IsUnit` `SubNegMonoid.toSub` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`eq_or_ne` `orderOf_eq_one_iff` `isUnit_neg_one` `zero_sub` `natCast_zmod_surjective` `orderOf_dvd_iff_pow_eq_one` `Nat.cast_pow` `Nat.cast_one` `natCast_eq_natCast_iff` `Mathlib.Tactic.Contrapose.contrapose₂` `Nat.cast_zero` `not_imp_comm` `Nat.Prime.coprime_pow_of_not_dvd` `Fact.out` `isUnit_iff_coprime` `Nat.cast_sub` `pow_pow_modEq_one` `add_comm` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le`
`expand_card` 📖	mathematical	—	`DFunLike.coe` `AlgHom` `ZMod` `Polynomial` `CommSemiring.toSemiring` `Semifield.toCommSemiring` `Field.toSemifield` `instField` `Polynomial.semiring` `Polynomial.algebraOfAlgebra` `Algebra.id` `AlgHom.funLike` `Polynomial.expand` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `FiniteField.expand_card` `card`
`fieldRange_castHom_eq_bot` 📖	mathematical	—	`RingHom.fieldRange` `ZMod` `Field.toDivisionRing` `instField` `castHom` `dvd_rfl` `Nat.instMonoid` `DivisionRing.toRing` `Bot.bot` `Subfield` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Subfield.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder`	—	`dvd_rfl` `RingHom.fieldRange_eq_map` `Subfield.map_bot` `instSubsingletonSubfield`
`frobenius_zmod` 📖	mathematical	—	`frobenius` `ZMod` `Semifield.toCommSemiring` `Field.toSemifield` `instField` `expChar_prime` `AddCommMonoidWithOne.toAddMonoidWithOne` `NonAssocSemiring.toAddCommMonoidWithOne` `Semiring.toNonAssocSemiring` `CommSemiring.toSemiring` `charP` `RingHom.id`	—	`RingHom.ext` `expChar_prime` `charP` `frobenius_def` `pow_card` `RingHom.id_apply`
`instSubsingletonSubfield` 📖	mathematical	—	`Subfield` `ZMod` `Field.toDivisionRing` `instField`	—	`subsingleton_of_bot_eq_top` `top_unique` `zsmul_mem` `SubringClass.addSubgroupClass` `SubfieldClass.toSubringClass` `Subfield.instSubfieldClass` `OneMemClass.one_mem` `AddSubmonoidWithOneClass.toOneMemClass` `SubsemiringClass.addSubmonoidWithOneClass` `SubringClass.toSubsemiringClass` `natCast_zmod_val` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Nat.smul_one_eq_cast` `natCast_zsmul`
`orderOf_dvd_card_sub_one` 📖	mathematical	—	`orderOf` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField`	—	`orderOf_dvd_of_pow_eq_one` `pow_card_sub_one_eq_one`
`orderOf_units_dvd_card_sub_one` 📖	mathematical	—	`orderOf` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `Units.instMonoid`	—	`orderOf_dvd_of_pow_eq_one` `units_pow_card_sub_one_eq_one`
`pow_card` 📖	mathematical	—	`ZMod` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `FiniteField.pow_card` `card`
`pow_card_pow` 📖	mathematical	—	`ZMod` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `Nat.instMonoid`	—	`pow_zero` `pow_one` `pow_succ` `pow_mul` `pow_card`
`pow_card_sub_one` 📖	mathematical	—	`ZMod` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `decidableEq` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`pow_card_sub_one_eq_one` `of_not_not` `zero_pow` `Nat.instCanonicallyOrderedAdd` `Nat.instOrderedSub` `Nat.Prime.one_lt` `Fact.out`
`pow_card_sub_one_eq_one` 📖	mathematical	—	`ZMod` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `AddMonoidWithOne.toOne` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `DivisionRing.toRing` `Field.toDivisionRing`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `FiniteField.pow_card_sub_one_eq_one` `card`
`pow_totient` 📖	mathematical	—	`Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `commRing` `Monoid.toNatPow` `Units.instMonoid` `Nat.totient` `Units.instOne`	—	`Nat.totient_zero` `pow_zero` `card_units_eq_totient` `pow_card_eq_one`
`sq_add_sq` 📖	mathematical	—	`ZMod` `Distrib.toAdd` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `commRing` `Monoid.toNatPow` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField`	—	`Nat.Prime.eq_two_or_odd` `Fact.out` `Fintype.complete` `zero_pow` `Nat.instCharZero` `Nat.instAtLeastTwoHAddOfNat` `zero_add` `isReduced_of_noZeroDivisors` `IsDomain.to_noZeroDivisors` `instIsDomain` `one_pow` `FiniteField.exists_root_sum_quadratic` `NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `Polynomial.degree_X_pow` `nontrivial` `Polynomial.degree_X_pow_sub_C` `card` `sub_eq_zero` `Polynomial.eval_pow` `Polynomial.eval_X` `Polynomial.eval_sub` `Polynomial.eval_C`
`units_pow_card_sub_one_eq_one` 📖	mathematical	—	`Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `DivisionSemiring.toSemiring` `Semifield.toDivisionSemiring` `Field.toSemifield` `instField` `Monoid.toNatPow` `Units.instMonoid` `Units.instOne`	—	`NeZero.of_gt'` `Nat.instCanonicallyOrderedAdd` `Nat.Prime.one_lt'` `card_units` `pow_card_eq_one`

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instFiniteZModUnits` 📖	mathematical	—	`Finite` `Units` `ZMod` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `ZMod.commRing`	—	`Finite.of_fintype` `instFiniteUnits`
`mem_bot_iff_intCast` 📖	mathematical	—	`Subfield` `SetLike.instMembership` `Subfield.instSetLike` `Bot.bot` `OrderBot.toBot` `Preorder.toLE` `PartialOrder.toPreorder` `SemilatticeSup.toPartialOrder` `Lattice.toSemilatticeSup` `CompleteLattice.toLattice` `Subfield.instCompleteLattice` `BoundedOrder.toOrderBot` `CompleteLattice.toBoundedOrder` `AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `DivisionRing.toRing`	—	`dvd_rfl` `ZMod.fieldRange_castHom_eq_bot` `Function.Surjective.exists` `ZMod.intCast_surjective` `ZMod.cast_intCast`
`pow_pow_modEq_one` 📖	mathematical	—	`Nat.ModEq` `Monoid.toNatPow` `Nat.instMonoid`	—	`Nat.modEq_one` `Nat.modEq_iff_dvd'` `Nat.one_le_pow'` `add_comm` `Nat.ModEq.comm` `pow_succ` `pow_mul` `tsub_eq_iff_eq_add_of_le` `CanonicallyOrderedAdd.toExistsAddOfLE` `Nat.instCanonicallyOrderedAdd` `IsOrderedAddMonoid.toAddLeftMono` `Nat.instIsOrderedAddMonoid` `Nat.instOrderedSub` `IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT` `AddLeftCancelSemigroup.toIsLeftCancelAdd` `contravariant_lt_of_covariant_le` `add_pow` `Finset.sum_range_succ'` `pow_zero` `one_mul` `one_pow` `Nat.choose_zero_right` `Nat.cast_one` `Nat.ModEq.add_right` `Nat.modEq_zero_iff_dvd` `Finset.sum_congr` `mul_one` `pow_succ'` `mul_assoc` `mul_dvd_mul_left` `dvd_mul_of_dvd_right` `Finset.dvd_sum` `AddRightCancelSemigroup.toIsRightCancelAdd` `pow_one` `zero_add` `Nat.choose_one_right`

---

← Back to Index