instance CharZero.subsemiring {A : Type u_2} [Semiring A] {S : Type u_3} [SetLike S A] [SubsemiringClass S A] [CharZero A] (x : S) : CharZero { x // x ∈ x }

Equations

• @CharZero.subsemiring = @CharZero.subsemiring.proof_1

instance instCharZeroSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToAddMonoidWithOneToAddGroupWithOneToRing {K : Type u_1} [Field K] [CharZero K] : CharZero { x // x ∈ NumberField.ringOfIntegers K }

Equations

• One or more equations did not get rendered due to their size.

theorem Ideal.isCoprime_iff_sup {R : Type u_2} [CommSemiring R] {I : Ideal R} {J : Ideal R} : IsCoprime I J ↔ I ⊔ J = ⊤

instance foofoo {K : Type u_1} [Field K] [NumberField K] : IsDomain (Ideal { x // x ∈ NumberField.ringOfIntegers K })

Equations

• @foofoo = @foofoo.proof_1

instance instCancelMonoidWithZeroIdealSubtypeMemSubalgebraIntToCommSemiringInstCommRingIntToSemiringToCommSemiringToCommRingToEuclideanDomainAlgebraIntToRingToDivisionRingInstMembershipInstSetLikeSubalgebraRingOfIntegersToSemiring {K : Type u_1} [Field K] [NumberField K] : CancelMonoidWithZero (Ideal { x // x ∈ NumberField.ringOfIntegers K })

Equations

• One or more equations did not get rendered due to their size.

theorem WfDvdMonoid.multiplicity_finite {M : Type u_2} [CancelCommMonoidWithZero M] [WfDvdMonoid M] {x : M} {y : M} (hx : ¬IsUnit x) (hy : y ≠ 0) : multiplicity.Finite x y

theorem WfDvdMonoid.multiplicity_finite_iff {M : Type u_2} [CancelCommMonoidWithZero M] [WfDvdMonoid M] {x : M} {y : M} : multiplicity.Finite x y ↔ ¬IsUnit x ∧ y ≠ 0

theorem WfDvdMonoid.multiplicity_eq_top_iff {M : Type u_2} [CancelCommMonoidWithZero M] [WfDvdMonoid M] [DecidableRel fun a b => a ∣ b] {x : M} {y : M} : multiplicity x y = ⊤ ↔ IsUnit x ∨ y = 0

theorem dvd_iff_multiplicity_le {M : Type u_2} [CancelCommMonoidWithZero M] [DecidableRel fun a b => a ∣ b] [UniqueFactorizationMonoid M] {a : M} {b : M} (ha : a ≠ 0) : a ∣ b ↔ ∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b

theorem ENat.mul_mono_left {k : ℕ∞} {n : ℕ∞} {m : ℕ∞} (hk : k ≠ 0) (hk' : k ≠ ⊤) : k * n ≤ k * m ↔ n ≤ m

theorem ENat.nsmul_mono {n : ℕ∞} {m : ℕ∞} {k : ℕ} (hk : k ≠ 0) : k • n ≤ k • m ↔ n ≤ m

theorem pow_dvd_pow_iff_dvd {M : Type u_2} [CancelCommMonoidWithZero M] [UniqueFactorizationMonoid M] {a : M} {b : M} {x : ℕ} (h' : x ≠ 0) : a ^ x ∣ b ^ x ↔ a ∣ b

theorem isPrincipal_of_isPrincipal_pow_of_Coprime' {A : Type u_2} {K : Type u_3} [CommRing A] [IsDedekindDomain A] [Fintype (ClassGroup A)] [Field K] [Algebra A K] [IsFractionRing A K] (p : ℕ) (H : Nat.Coprime p (Fintype.card (ClassGroup A))) (I : FractionalIdeal (nonZeroDivisors A) K) (hI : Submodule.IsPrincipal ↑(I ^ p)) : Submodule.IsPrincipal ↑I

theorem mul_mem_nthRootsFinset {R : Type u_2} {n : ℕ} [CommRing R] [IsDomain R] {η₁ : R} (hη₁ : η₁ ∈ Polynomial.nthRootsFinset n R) {η₂ : R} (hη₂ : η₂ ∈ Polynomial.nthRootsFinset n R) : η₁ * η₂ ∈ Polynomial.nthRootsFinset n R

theorem ne_zero_of_mem_nthRootsFinset {R : Type u_2} {n : ℕ} [CommRing R] [IsDomain R] {η : R} (hη : η ∈ Polynomial.nthRootsFinset n R) : η ≠ 0

theorem IsPrimitiveRoot.prime_span_sub_one {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (hp : p ≠ 2) : Prime (Ideal.span {↑(IsPrimitiveRoot.unit' hζ) - 1})

theorem norm_Int_zeta_sub_one {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (hp : p ≠ 2) : ↑(Algebra.norm ℤ) (↑(IsPrimitiveRoot.unit' hζ) - 1) = ↑↑p

theorem one_mem_nthRootsFinset {R : Type u_2} {n : ℕ} [CommRing R] [IsDomain R] (hn : 0 < n) : 1 ∈ Polynomial.nthRootsFinset n R

theorem associated_zeta_sub_one_pow_prime {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) : Associated ((↑(IsPrimitiveRoot.unit' hζ) - 1) ^ (↑p - 1)) ↑↑p

theorem isCoprime_of_not_zeta_sub_one_dvd {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (hp : p ≠ 2) {x : { x // x ∈ NumberField.ringOfIntegers K }} (hx : ¬↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ x) : IsCoprime (↑↑p) x

theorem exists_zeta_sub_one_dvd_sub_Int {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (a : { x // x ∈ NumberField.ringOfIntegers K }) : ∃ b, ↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ a - ↑b

theorem exists_dvd_pow_sub_Int_pow {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] (hp : p ≠ 2) (a : { x // x ∈ NumberField.ringOfIntegers K }) : ∃ b, ↑↑p ∣ a ^ ↑p - ↑b ^ ↑p

theorem norm_dvd_iff {R : Type u_2} [CommRing R] [IsDomain R] [IsDedekindDomain R] [Infinite R] [Module.Free ℤ R] [Module.Finite ℤ R] (x : R) (hx : Prime (↑(Algebra.norm ℤ) x)) {y : ℤ} : ↑(Algebra.norm ℤ) x ∣ y ↔ x ∣ ↑y

theorem exists_not_dvd_spanSingleton_eq {R : Type u_2} [CommRing R] [IsDomain R] [IsDedekindDomain R] {K : Type u_3} [Field K] [Algebra R K] [IsFractionRing R K] {x : R} (hx : Prime x) (I : Ideal R) (J : Ideal R) (hI : ¬Ideal.span {x} ∣ I) (hJ : ¬Ideal.span {x} ∣ J) (h : Submodule.IsPrincipal ↑(↑I / ↑J)) : ∃ a b, ¬x ∣ a ∧ ¬x ∣ b ∧ FractionalIdeal.spanSingleton (nonZeroDivisors R) (↑(algebraMap R K) a / ↑(algebraMap R K) b) = ↑I / ↑J

theorem zeta_sub_one_dvd_Int_iff {K : Type u_1} {p : ℕ+} [hpri : Fact (PNat.Prime p)] [Field K] [CharZero K] [IsCyclotomicExtension {p} ℚ K] {ζ : K} (hζ : IsPrimitiveRoot ζ ↑p) (hp : p ≠ 2) {n : ℤ} : ↑(IsPrimitiveRoot.unit' hζ) - 1 ∣ ↑n ↔ ↑↑p ∣ n