PID

📁 Source: Mathlib/NumberTheory/NumberField/Cyclotomic/PID.lean

Statistics

Metric	Count
Definitions	0
Theorems five_pid, three_pid	2
Total	2

IsCyclotomicExtension.Rat

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
five_pid 📖	mathematical	—	IsPrincipalIdealRing NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing	—	NumberField.to_charZero Nat.prime_five RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt Nat.instAtLeastTwoHAddOfNat IsCyclotomicExtension.numberField Rat.numberField Finite.of_fintype discr_prime IsCyclotomicExtension.finrank instIsDomain Polynomial.cyclotomic.irreducible_rat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial nrComplexPlaces_eq_totient_div_two Nat.totient_prime tsub_zero Nat.instOrderedSub Even.neg_pow one_pow one_mul Int.cast_abs Real.instIsStrictOrderedRing Int.cast_ofNat abs_of_pos IsOrderedAddMonoid.toAddLeftMono Real.instIsOrderedAddMonoid Real.instIsOrderedRing Real.instNontrivial div_pow pow_lt_pow_left₀ IsStrictOrderedRing.toPosMulStrictMono IsOrderedRing.toMulPosMono mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono mul_lt_mul_of_pos_left div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE Real.pi_gt_three le_of_lt Mathlib.Meta.Positivity.pos_of_isNat Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo ne_of_gt pow_pos IsStrictOrderedRing.toZeroLEOneClass div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE mul_pos lt_trans Mathlib.Meta.NormNum.isNat_lt_true RCLike.charZero_rclike Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0 Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNatPowT.trans
three_pid 📖	mathematical	—	IsPrincipalIdealRing NumberField.RingOfIntegers CommSemiring.toSemiring CommRing.toCommSemiring NumberField.RingOfIntegers.instCommRing	—	NumberField.to_charZero RingOfIntegers.isPrincipalIdealRing_of_abs_discr_lt Nat.instAtLeastTwoHAddOfNat IsCyclotomicExtension.numberField Rat.numberField Finite.of_fintype discr_prime Nat.fact_prime_three IsCyclotomicExtension.finrank instIsDomain Polynomial.cyclotomic.irreducible_rat IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial nrComplexPlaces_eq_totient_div_two Nat.totient_prime Nat.prime_three tsub_zero Nat.instOrderedSub Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid pow_one neg_mul one_mul abs_neg Int.cast_abs Real.instIsStrictOrderedRing Int.cast_ofNat abs_of_pos Real.instIsOrderedAddMonoid zero_lt_three' Real.instZeroLEOneClass NeZero.charZero_one RCLike.charZero_rclike pow_lt_pow_left₀ IsStrictOrderedRing.toPosMulStrictMono IsOrderedRing.toMulPosMono Real.instIsOrderedRing mul_lt_mul_of_pos_right IsStrictOrderedRing.toMulPosStrictMono mul_lt_mul_of_pos_left div_lt_div_of_pos_right MulPosReflectLE.toMulPosReflectLT MulPosStrictMono.toMulPosReflectLE Real.pi_gt_three Mathlib.Meta.Positivity.pos_of_isNat Real.instNontrivial Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo div_pos PosMulReflectLE.toPosMulReflectLT PosMulStrictMono.toPosMulReflectLE pow_pos IsStrictOrderedRing.toZeroLEOneClass le_of_lt mul_pos ne_of_gt lt_trans Mathlib.Meta.NormNum.isNat_lt_true Mathlib.Meta.NormNum.isNat_pow Mathlib.Meta.NormNum.IsNNRat.to_isNat Mathlib.Meta.NormNum.isNNRat_mul Mathlib.Meta.NormNum.IsNat.to_isNNRat Mathlib.Meta.NormNum.isNNRat_div Mathlib.Meta.NormNum.isNNRat_inv_pos Mathlib.Meta.NormNum.IsNatPowT.run Mathlib.Meta.NormNum.IsNatPowT.bit0

---

← Back to Index