GaloisField

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

Statistics

Metric	Count
Definitions algEquivOfCardEq, ringEquivOfCardEq, GaloisField, algEquivGaloisField, algEquivGaloisFieldOfFintype, equivZmodP, instAlgebraZModGaloisField, instCharPGaloisField, instFieldGaloisField, instFiniteDimensionalZModGaloisField, instFiniteGaloisField, instInhabitedGaloisField, instIsSplittingFieldZModGaloisFieldHSubPolynomialHPowNatX	13
Theorems algebraMap_norm_eq_pow, card_algHom_of_finrank_dvd, isSplittingField_of_card_eq, isSplittingField_of_nat_card_eq, isSplittingField_sub, natCard_algHom_of_finrank_dvd, nonempty_algHom_iff_finrank_dvd, nonempty_algHom_of_finrank_dvd, norm_surjective, pow_finrank_eq_card, pow_finrank_eq_natCard, splits_X_pow_card_sub_X, splits_X_pow_nat_card_sub_X, unitsMap_norm_surjective, card, finrank, instIsGaloisOfFinite, splits_zmod_X_pow_sub_X, splits_X_pow_nat_card_sub_X, galois_poly_separable	20
Total	33

FiniteField

Definitions

Name	Category	Theorems
algEquivOfCardEq 📖	CompOp	—
ringEquivOfCardEq 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_norm_eq_pow 📖	mathematical	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Nat.card	—	Finite.of_injective RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Algebra.norm_eq_prod_automorphisms GaloisField.instIsGaloisOfFinite Algebra.IsAlgebraic.of_finite Function.Bijective.prod_comp bijective_frobeniusAlgEquivOfAlgebraic_pow Finset.prod_congr AlgEquiv.coe_pow pow_iterate Finset.prod_pow_eq_pow_sum Fin.sum_univ_eq_sum_range Nat.geomSum_eq Fintype.one_lt_card
card_algHom_of_finrank_dvd 📖	mathematical	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	Fintype.card AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring minpoly.AlgHom.fintype DivisionRing.toRing Field.toDivisionRing EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Module.instFiniteDimensionalOfIsReflexive Ring.toAddCommGroup Algebra.toModule Ring.toSemiring Module.instIsReflexiveOfFiniteOfProjective AddCommGroup.toAddCommMonoid Module.IsNoetherian.finite CommSemiring.toSemiring isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	instIsDomain Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Fintype.card_eq_nat_card natCard_algHom_of_finrank_dvd
isSplittingField_of_card_eq 📖	mathematical	Fintype.card Monoid.toPow Nat.instMonoid	Polynomial.IsSplittingField ZMod ZMod.instField Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Nat.instMonoid	—	isSplittingField_sub
isSplittingField_of_nat_card_eq 📖	mathematical	Nat.card Monoid.toPow Nat.instMonoid	Polynomial.IsSplittingField ZMod ZMod.instField Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Nat.instMonoid	—	Nat.card_pos_iff pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono Nat.instZeroLEOneClass Nat.Prime.pos Fact.out Nat.card_eq_fintype_card isSplittingField_sub
isSplittingField_sub 📖	mathematical	—	Polynomial.IsSplittingField Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Fintype.card	—	X_pow_card_sub_X_natDegree_eq Fintype.one_lt_card IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain Polynomial.splits_iff_card_roots Polynomial.map_sub Polynomial.map_pow Polynomial.map_X roots_X_pow_card_sub_X Finset.card_def Finset.card_univ Polynomial.roots.congr_simp Finset.val_toFinset Finset.coe_univ Algebra.adjoin_univ
natCard_algHom_of_finrank_dvd 📖	mathematical	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	Nat.card AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule	—	nonempty_algHom_of_finrank_dvd Finite.of_injective RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Nat.card_congr IsScalarTower.of_algHom IsGalois.to_normal GaloisField.instIsGaloisOfFinite IsGalois.card_aut_eq_finrank Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing
nonempty_algHom_iff_finrank_dvd 📖	mathematical	—	AlgHom Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring Module.finrank NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain Algebra.toModule	—	Module.finrank_mul_finrank IsScalarTower.of_algHom commRing_strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing dvd_mul_right nonempty_algHom_of_finrank_dvd
nonempty_algHom_of_finrank_dvd 📖	mathematical	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 Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	Finite.of_injective RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Module.finite_of_finrank_pos commRing_strongRankCondition Module.Free.of_divisionRing Module.finrank_pos Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_finite Module.Projective.of_free instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors Module.finite_of_finite isSplittingField_sub Polynomial.Splits.of_dvd Polynomial.IsSplittingField.splits Polynomial.map_ne_zero X_pow_card_sub_X_ne_zero Fintype.one_lt_card Module.card_eq_pow_finrank Polynomial.map_dvd_map' dvd_pow_pow_sub_self_of_dvd
norm_surjective 📖	mathematical	—	DFunLike.coe MonoidHom MulOneClass.toMulOne MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Ring.toSemiring DivisionRing.toRing Field.toDivisionRing CommSemiring.toSemiring CommRing.toCommSemiring EuclideanDomain.toCommRing Field.toEuclideanDomain MonoidHom.instFunLike Algebra.norm	—	eq_or_ne Algebra.norm_zero IsLocalRing.toNontrivial Field.instIsLocalRing Module.Free.of_divisionRing Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free unitsMap_norm_surjective
pow_finrank_eq_card 📖	mathematical	—	Monoid.toPow Nat.instMonoid Module.finrank ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField AddCommGroup.toAddCommMonoid Fintype.card	—	pow_finrank_eq_natCard Finite.of_fintype Fintype.card_eq_nat_card
pow_finrank_eq_natCard 📖	mathematical	—	Monoid.toPow Nat.instMonoid Module.finrank ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField AddCommGroup.toAddCommMonoid Nat.card	—	Module.natCard_eq_pow_finrank Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Nat.card_zmod
splits_X_pow_card_sub_X 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map ZMod ZMod.instField algebraMap Semifield.toCommSemiring Polynomial Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Fintype.card	—	Polynomial.IsSplittingField.splits isSplittingField_sub
splits_X_pow_nat_card_sub_X 📖	mathematical	—	Polynomial.Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.map ZMod ZMod.instField algebraMap Semifield.toCommSemiring Polynomial Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X Nat.card	—	Nat.card_eq_fintype_card Polynomial.IsSplittingField.splits isSplittingField_sub
unitsMap_norm_surjective 📖	mathematical	—	Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe MonoidHom MulOneClass.toMulOne Units.instMulOneClass MonoidHom.instFunLike Units.map Algebra.norm EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	—	Finite.of_injective_finite_range RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Subtype.finite MonoidHom.surjective_of_card_ker_le_div instFiniteUnits Nat.card_units Set.ncard_coe_finset SetLike.coe_sort_coe Nat.card_coe_set_eq Set.ext algebraMap_norm_eq_pow map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Finset.filter.congr_simp Finset.coe_filter IsCyclic.card_pow_eq_one_le instIsCyclicUnitsOfFinite instIsDomain Nat.card_le_card_of_injective Finite.one_lt_card

GaloisField

Definitions

Name	Category	Theorems
algEquivGaloisField 📖	CompOp	—
algEquivGaloisFieldOfFintype 📖	CompOp	—
equivZmodP 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
card 📖	mathematical	—	Nat.card GaloisField Monoid.toPow Nat.instMonoid	—	isNoetherian_of_isNoetherianRing_of_finite PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Module.instFiniteDimensionalOfIsReflexive Module.instIsReflexiveOfFiniteOfProjective Module.IsNoetherian.finite isNoetherian_of_finite Module.Projective.of_free Module.Free.of_divisionRing Nat.card_eq_fintype_card NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' Module.card_fintype Module.finrank_eq_card_basis commRing_strongRankCondition ZMod.nontrivial ZMod.card finrank
finrank 📖	mathematical	—	Module.finrank ZMod GaloisField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain instFieldGaloisField Algebra.toModule Semifield.toCommSemiring instAlgebraZModGaloisField	—	Nat.Prime.one_lt Fact.out FiniteField.X_pow_card_pow_sub_X_ne_zero instIsDomain Polynomial.card_rootSet_eq_natDegree galois_poly_separable ZMod.charP dvd_pow dvd_refl Polynomial.SplittingField.splits FiniteField.X_pow_card_pow_sub_X_natDegree_eq Set.eq_univ_iff_forall Polynomial.SplittingField.adjoin_rootSet Subring.closure_induction Polynomial.mem_rootSet_of_ne ZMod.instIsDomain instIsTorsionFreeOfIsDomainOfNoZeroSMulDivisors GroupWithZero.toNoZeroSMulDivisors map_sub DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_X RingHom.instRingHomClass ZMod.pow_card_pow sub_self Polynomial.IsSplittingField.instIsTorsionFreeSplittingField Polynomial.coeff_zero_eq_aeval_zero' Polynomial.coeff_sub Polynomial.coeff_X_pow Polynomial.coeff_X_zero sub_zero IsLocalRing.toNontrivial Field.instIsLocalRing NeZero.one ZMod.nontrivial Nat.Prime.one_lt' eq_zero_of_pow_eq_zero isReduced_of_noZeroDivisors IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd Polynomial.aeval_sub one_pow Polynomial.aeval_X_pow add_pow_char_pow sub_neg_eq_add neg_pow neg_one_pow_char_pow neg_mul one_mul neg_add_cancel mul_pow Nat.pow_right_injective NeZero.of_gt' ZMod.card Module.card_eq_pow_finrank Fintype.ofEquiv_card Fintype.card_congr'
instIsGaloisOfFinite 📖	mathematical	—	IsGalois	—	nonempty_fintype CharP.exists IsGalois.of_separable_splitting_field FiniteField.isSplittingField_sub galois_poly_separable FiniteField.card charP_of_injective_algebraMap' Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing IsLocalRing.toNontrivial Field.instIsLocalRing dvd_pow_self PNat.ne_zero
splits_zmod_X_pow_sub_X 📖	mathematical	—	Polynomial.Splits ZMod DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield ZMod.instField Polynomial Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X	—	Nat.Prime.one_lt Fact.out ZMod.instIsDomain NeZero.of_gt' Nat.instCanonicallyOrderedAdd Nat.Prime.one_lt' instIsDomain ZMod.card FiniteField.roots_X_pow_card_sub_X FiniteField.X_pow_card_sub_X_natDegree_eq Polynomial.splits_iff_card_roots Finset.card_def Finset.card_univ

Polynomial

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
splits_X_pow_nat_card_sub_X 📖	mathematical	—	Splits DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial instSub DivisionRing.toRing Field.toDivisionRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X Nat.card	—	IsSplittingField.splits FiniteField.isSplittingField_sub Nat.card_eq_fintype_card map_sub map_pow map_X splits_neg_iff Nat.card_eq_zero_of_infinite pow_zero neg_sub map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Splits.X_sub_C

(root)

Definitions

Name	Category	Theorems
GaloisField 📖	CompOp	2 math math: GaloisField.finrank, GaloisField.card
instAlgebraZModGaloisField 📖	CompOp	1 math math: GaloisField.finrank
instCharPGaloisField 📖	CompOp	—
instFieldGaloisField 📖	CompOp	1 math math: GaloisField.finrank
instFiniteDimensionalZModGaloisField 📖	CompOp	—
instFiniteGaloisField 📖	CompOp	—
instInhabitedGaloisField 📖	CompOp	—
instIsSplittingFieldZModGaloisFieldHSubPolynomialHPowNatX 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
galois_poly_separable 📖	mathematical	—	Polynomial.Separable CommRing.toCommSemiring Polynomial CommSemiring.toSemiring Polynomial.instSub CommRing.toRing Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.X	—	Polynomial.derivative_sub Polynomial.derivative_X_pow Polynomial.derivative_X Polynomial.C_eq_natCast CharP.cast_eq_zero_iff Polynomial.instCharP Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.cast_zero Nat.cast_zero Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_overlap_zero Mathlib.Tactic.Ring.add_overlap_pf_zero Mathlib.Meta.NormNum.isInt_add

---

← Back to Index