Skip to content
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion Archive/Imo/Imo1961Q3.lean
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ theorem Imo1961Q3 {n : ℕ} {x : ℝ} (h₀ : n ≠ 0) :
simp [hsinx, hcosx] at this
| 2 =>
rw [← cos_sq_add_sin_sq x, sub_eq_add_neg, add_right_inj, neg_eq_self ℝ] at h
exact absurd (pow_eq_zero h) hsinx
exact absurd (eq_zero_of_pow_eq_zero h) hsinx
| (n + 1 + 2) =>
set m := n + 1
refine absurd ?_ h.not_lt
Expand Down
2 changes: 1 addition & 1 deletion Archive/Imo/Imo1962Q4.lean
Original file line number Diff line number Diff line change
Expand Up @@ -96,7 +96,7 @@ theorem formula {R : Type*} [CommRing R] [IsDomain R] [CharZero R] (a : R) :
a ^ 2 + ((2 : R) * a ^ 2 - (1 : R)) ^ 2 + ((4 : R) * a ^ 3 - 3 * a) ^ 2 = 1 ↔
((2 : R) * a ^ 2 - (1 : R)) * ((4 : R) * a ^ 3 - 3 * a) = 0 := by
constructor <;> intro h
· apply pow_eq_zero (n := 2)
· apply eq_zero_of_pow_eq_zero (n := 2)
apply mul_left_injective₀ (b := 2) (by simp)
linear_combination (8 * a ^ 4 - 10 * a ^ 2 + 3) * h
· linear_combination 2 * a * h
Expand Down
10 changes: 6 additions & 4 deletions Mathlib/Algebra/GroupWithZero/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -166,16 +166,18 @@ lemma pow_mul_eq_zero_of_le {a b : M₀} {m n : ℕ} (hmn : m ≤ n)

variable [NoZeroDivisors M₀]

lemma pow_eq_zero : ∀ {n}, a ^ n = 0 → a = 0
lemma eq_zero_of_pow_eq_zero : ∀ {n}, a ^ n = 0 → a = 0
| 0, ha => by simpa using congr_arg (a * ·) ha
| n + 1, ha => by rw [pow_succ, mul_eq_zero] at ha; exact ha.elim pow_eq_zero id
| n + 1, ha => by rw [pow_succ, mul_eq_zero] at ha; exact ha.elim eq_zero_of_pow_eq_zero id

@[deprecated (since := "2025-10-14")] alias pow_eq_zero := eq_zero_of_pow_eq_zero

@[simp] lemma pow_eq_zero_iff (hn : n ≠ 0) : a ^ n = 0 ↔ a = 0 :=
pow_eq_zero, by rintro rfl; exact zero_pow hn⟩
eq_zero_of_pow_eq_zero, by rintro rfl; exact zero_pow hn⟩

lemma pow_ne_zero_iff (hn : n ≠ 0) : a ^ n ≠ 0 ↔ a ≠ 0 := (pow_eq_zero_iff hn).not

lemma pow_ne_zero (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 := mt pow_eq_zero h
lemma pow_ne_zero (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 := mt eq_zero_of_pow_eq_zero h

instance NeZero.pow [NeZero a] : NeZero (a ^ n) := ⟨pow_ne_zero n NeZero.out⟩

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
Original file line number Diff line number Diff line change
Expand Up @@ -205,7 +205,7 @@ theorem le_nonZeroDivisors_of_noZeroDivisors {S : Submonoid M₀} (hS : (0 : M
mem_nonZeroDivisors_of_ne_zero <| by rintro rfl; exact hS hx

theorem powers_le_nonZeroDivisors_of_noZeroDivisors (hx : x ≠ 0) : Submonoid.powers x ≤ M₀⁰ :=
le_nonZeroDivisors_of_noZeroDivisors fun h ↦ hx (h.recOn fun _ ↦ pow_eq_zero)
le_nonZeroDivisors_of_noZeroDivisors fun h ↦ hx (h.recOn fun _ ↦ eq_zero_of_pow_eq_zero)

end NoZeroDivisors

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/IsPrimePow.lean
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ theorem isPrimePow_iff_pow_succ : IsPrimePow n ↔ ∃ (p : R) (k : ℕ), Prime
theorem not_isPrimePow_zero [NoZeroDivisors R] : ¬IsPrimePow (0 : R) := by
simp only [isPrimePow_def, not_exists, not_and', and_imp]
intro x n _hn hx
rw [pow_eq_zero hx]
rw [eq_zero_of_pow_eq_zero hx]
simp

theorem IsPrimePow.not_unit {n : R} (h : IsPrimePow n) : ¬IsUnit n :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Polynomial/DenomsClearable.lean
Original file line number Diff line number Diff line change
Expand Up @@ -96,5 +96,5 @@ theorem one_le_pow_mul_abs_eval_div {K : Type*} [Field K] [LinearOrder K] [IsStr
refine Int.le_of_lt_add_one ((lt_add_iff_pos_left 1).mpr (abs_pos.mpr fun F0 => fab ?_))
rw [eq_one_div_of_mul_eq_one_left bu, F0, one_div, eq_intCast, Int.cast_zero, zero_eq_mul] at hF
rcases hF with hF | hF
· exact (not_le.mpr b0 (le_of_eq (Int.cast_eq_zero.mp (pow_eq_zero hF)))).elim
· exact (not_le.mpr b0 (le_of_eq (Int.cast_eq_zero.mp (eq_zero_of_pow_eq_zero hF)))).elim
· rwa [div_eq_mul_inv]
2 changes: 1 addition & 1 deletion Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean
Original file line number Diff line number Diff line change
Expand Up @@ -204,7 +204,7 @@ theorem aeval_sumIDeriv_of_pos [Nontrivial A] [NoZeroDivisors A] (p : R[X]) {q :
rw [Polynomial.map_zero] at hp
replace hp := (mul_eq_zero.mp hp.symm).resolve_left ?_
· rw [hp, eval_zero, smul_zero]
exact fun h => X_sub_C_ne_zero r (pow_eq_zero h)
exact fun h => X_sub_C_ne_zero r (eq_zero_of_pow_eq_zero h)
let c k := if hk : q ≤ k then (aeval_iterate_derivative_of_ge A p q hk).choose else 0
have c_le (k) : (c k).natDegree ≤ p.natDegree - k := by
dsimp only [c]
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/Algebra/Quaternion.lean
Original file line number Diff line number Diff line change
Expand Up @@ -1266,7 +1266,8 @@ theorem normSq_eq_zero : normSq a = 0 ↔ a = 0 := by
refine ⟨fun h => ?_, fun h => h.symm ▸ normSq.map_zero⟩
rw [normSq_def', add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg, add_eq_zero_iff_of_nonneg]
at h
· exact ext a 0 (pow_eq_zero h.1.1.1) (pow_eq_zero h.1.1.2) (pow_eq_zero h.1.2) (pow_eq_zero h.2)
· apply ext a 0 <;> apply eq_zero_of_pow_eq_zero
exacts [h.1.1.1, h.1.1.2, h.1.2, h.2]
all_goals apply_rules [sq_nonneg, add_nonneg]

theorem normSq_ne_zero : normSq a ≠ 0 ↔ a ≠ 0 := normSq_eq_zero.not
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -439,7 +439,7 @@ lemma Y_ne_zero_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Nonsi
have hPx : P x ≠ 0 := X_ne_zero_of_Z_eq_zero hP hPz
intro hPy
rw [nonsingular_of_Z_eq_zero hPz, equation_of_Z_eq_zero hPz, hPy, zero_pow two_ne_zero] at hP
exact hPx <| pow_eq_zero hP.left.symm
exact hPx <| eq_zero_of_pow_eq_zero hP.left.symm

lemma isUnit_Y_of_Z_eq_zero {P : Fin 3 → F} (hP : W.Nonsingular P) (hPz : P z = 0) : IsUnit (P y) :=
(Y_ne_zero_of_Z_eq_zero hP hPz).isUnit
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -280,7 +280,7 @@ lemma equation_of_Z_ne_zero {P : Fin 3 → F} (hPz : P z ≠ 0) :

lemma X_eq_zero_of_Z_eq_zero [NoZeroDivisors R] {P : Fin 3 → R} (hP : W'.Equation P)
(hPz : P z = 0) : P x = 0 :=
pow_eq_zero <| (equation_of_Z_eq_zero hPz).mp hP
eq_zero_of_pow_eq_zero <| (equation_of_Z_eq_zero hPz).mp hP

/-! ## The nonsingular condition in projective coordinates -/

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -284,7 +284,7 @@ lemma spectrum_star_mul_self_nonneg {b : A} : ∀ x ∈ spectrum ℝ (star b * b
rw [h_c_spec₁.mul_comm.eq_zero_of_neg (.star_mul_self c) h_c_spec₀, neg_zero, CFC.negPart_def,
cfcₙ_eq_cfc (hf0 := by simp), ← cfc_pow _ _ (ha := ha), ← cfc_zero a (R := ℝ)] at h_eq_negPart_a
have h_eqOn := eqOn_of_cfc_eq_cfc (ha := ha) h_eq_negPart_a
exact fun x hx ↦ negPart_eq_zero.mp <| pow_eq_zero (h_eqOn hx).symm
exact fun x hx ↦ negPart_eq_zero.mp <| eq_zero_of_pow_eq_zero (h_eqOn hx).symm

lemma IsSelfAdjoint.coe_mem_spectrum_complex {A : Type*} [TopologicalSpace A] [Ring A]
[StarRing A] [Algebra ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal]
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Analysis/InnerProductSpace/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -188,7 +188,7 @@ def InnerProductSpace.toCore [NormedAddCommGroup E] [c : InnerProductSpace 𝕜
rw [← InnerProductSpace.norm_sq_eq_re_inner]
apply sq_nonneg
definite := fun x hx =>
norm_eq_zero.1 <| pow_eq_zero (n := 2) <| by
norm_eq_zero.1 <| eq_zero_of_pow_eq_zero (n := 2) <| by
rw [InnerProductSpace.norm_sq_eq_re_inner (𝕜 := 𝕜) x, hx, map_zero] }

namespace InnerProductSpace.Core
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -382,7 +382,7 @@ theorem log_nat_eq_sum_factorization (n : ℕ) :
· simp only [← log_pow, ← Nat.cast_pow]
rw [← Finsupp.log_prod, ← Nat.cast_finsuppProd, Nat.factorization_prod_pow_eq_self hn]
intro p hp
rw [pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]
rw [eq_zero_of_pow_eq_zero (Nat.cast_eq_zero.1 hp), Nat.factorization_zero_right]

theorem tendsto_pow_log_div_mul_add_atTop (a b : ℝ) (n : ℕ) (ha : a ≠ 0) :
Tendsto (fun x => log x ^ n / (a * x + b)) atTop (𝓝 0) :=
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Analysis/SpecialFunctions/Trigonometric/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -767,7 +767,7 @@ theorem cos_pi_div_three : cos (π / 3) = 1 / 2 := by
ring
linarith [cos_pi, cos_three_mul (π / 3)]
rcases mul_eq_zero.mp h₁ with h | h
· linarith [pow_eq_zero h]
· linarith [eq_zero_of_pow_eq_zero h]
· have : cos π < cos (π / 3) := by
refine cos_lt_cos_of_nonneg_of_le_pi ?_ le_rfl ?_ <;> linarith [pi_pos]
linarith [cos_pi]
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Analysis/SpecificLimits/Normed.lean
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ theorem tendsto_intCast_atTop_cobounded
theorem isLittleO_pow_pow_of_lt_left {r₁ r₂ : ℝ} (h₁ : 0 ≤ r₁) (h₂ : r₁ < r₂) :
(fun n : ℕ ↦ r₁ ^ n) =o[atTop] fun n ↦ r₂ ^ n :=
have H : 0 < r₂ := h₁.trans_lt h₂
(isLittleO_of_tendsto fun _ hn ↦ False.elim <| H.ne' <| pow_eq_zero hn) <|
(isLittleO_of_tendsto fun _ hn ↦ False.elim <| H.ne' <| eq_zero_of_pow_eq_zero hn) <|
(tendsto_pow_atTop_nhds_zero_of_lt_one
(div_nonneg h₁ (h₁.trans h₂.le)) ((div_lt_one H).2 h₂)).congr fun _ ↦ div_pow _ _ _

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/FieldTheory/Finite/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -130,7 +130,7 @@ theorem card_cast_subgroup_card_ne_zero [Ring K] [NoZeroDivisors K] [Nontrivial
-- u ^ p = 1 implies (u - 1) ^ p = 0 and hence u = 1 ...
have h : u = 1 := by
rw [← sub_left_inj, sub_self 1]
apply pow_eq_zero (n := p)
apply eq_zero_of_pow_eq_zero (n := p)
rw [sub_pow_char_of_commute, one_pow, ← hu, pow_orderOf_eq_one, sub_self]
exact Commute.one_right u
-- ... meaning x didn't have order p after all, contradiction
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/FieldTheory/Finite/GaloisField.lean
Original file line number Diff line number Diff line change
Expand Up @@ -107,7 +107,7 @@ theorem finrank {n} (h : n ≠ 0) : Module.finrank (ZMod p) (GaloisField p n) =
simp only [coeff_X_pow, coeff_X_zero, sub_zero, _root_.map_eq_zero, ite_eq_right_iff,
one_ne_zero, coeff_sub]
intro hn
exact Nat.not_lt_zero 1 (pow_eq_zero hn.symm ▸ hp)
exact Nat.not_lt_zero 1 (eq_zero_of_pow_eq_zero hn.symm ▸ hp)
· simp
· simp only [aeval_X_pow, aeval_X, map_sub, add_pow_char_pow, sub_eq_zero]
intro x y _ _ hx hy
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/FieldTheory/PurelyInseparable/Tower.lean
Original file line number Diff line number Diff line change
Expand Up @@ -84,7 +84,7 @@ theorem LinearIndependent.map_of_isPurelyInseparable_of_isSeparable [IsPurelyIns
Finsupp.onFinset_sum _ (fun _ ↦ by exact zero_smul _ _)]
refine Finset.sum_congr rfl fun i _ ↦ ?_
simp_rw [Algebra.smul_def, mul_pow, IsScalarTower.algebraMap_apply F E K, hlF, map_pow]
refine pow_eq_zero ((hlF _).symm.trans ?_)
refine eq_zero_of_pow_eq_zero ((hlF _).symm.trans ?_)
convert map_zero (algebraMap F E)
exact congr($h i)

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/GroupTheory/Schreier.lean
Original file line number Diff line number Diff line change
Expand Up @@ -220,6 +220,6 @@ instance [Finite (commutatorSet G)] : Finite (_root_.commutator G) := by
have h2 := card_commutator_dvd_index_center_pow (closureCommutatorRepresentatives G)
refine Nat.finite_of_card_ne_zero fun h => ?_
rw [card_commutator_closureCommutatorRepresentatives, h, zero_dvd_iff] at h2
exact FiniteIndex.index_ne_zero (pow_eq_zero h2)
exact FiniteIndex.index_ne_zero (eq_zero_of_pow_eq_zero h2)

end Subgroup
2 changes: 1 addition & 1 deletion Mathlib/LinearAlgebra/SesquilinearForm/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -977,7 +977,7 @@ lemma apply_apply_same_eq_zero_iff (hs : ∀ x, 0 ≤ B x x) (hB : B.IsSymm) {x
ext y
have := B.apply_sq_le_of_symm hs hB x y
simp only [h, zero_mul] at this
exact pow_eq_zero <| le_antisymm this (sq_nonneg (B x y))
exact eq_zero_of_pow_eq_zero <| le_antisymm this (sq_nonneg (B x y))

lemma nondegenerate_iff (hs : ∀ x, 0 ≤ B x x) (hB : B.IsSymm) :
B.Nondegenerate ↔ ∀ x, B x x = 0 ↔ x = 0 := by
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/MeasureTheory/Function/ConvergenceInMeasure.lean
Original file line number Diff line number Diff line change
Expand Up @@ -188,7 +188,7 @@ theorem exists_nat_measure_lt_two_inv (hfg : TendstoInMeasure μ f atTop g) (n :
∃ N, ∀ m ≥ N, μ { x | (2 : ℝ≥0∞)⁻¹ ^ n ≤ edist (f m x) (g x) } ≤ (2⁻¹ : ℝ≥0∞) ^ n := by
specialize hfg ((2⁻¹ : ℝ≥0∞) ^ n) (ENNReal.pow_pos (by simp) _)
rw [ENNReal.tendsto_atTop_zero] at hfg
exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr fun h_zero => by simpa using pow_eq_zero h_zero)
exact hfg ((2 : ℝ≥0∞)⁻¹ ^ n) (pos_iff_ne_zero.mpr <| pow_ne_zero _ <| by simp)

/-- Given a sequence of functions `f` which converges in measure to `g`,
`seqTendstoAeSeqAux` is a sequence such that
Expand Down
3 changes: 1 addition & 2 deletions Mathlib/MeasureTheory/Measure/Lebesgue/EqHaar.lean
Original file line number Diff line number Diff line change
Expand Up @@ -340,8 +340,7 @@ theorem map_addHaar_smul {r : ℝ} (hr : r ≠ 0) :
change Measure.map f μ = _
have hf : LinearMap.det f ≠ 0 := by
simp only [f, mul_one, LinearMap.det_smul, Ne, MonoidHom.map_one]
intro h
exact hr (pow_eq_zero h)
exact pow_ne_zero _ hr
simp only [f, map_linearMap_addHaar_eq_smul_addHaar μ hf, mul_one, LinearMap.det_smul, map_one]

theorem quasiMeasurePreserving_smul {r : ℝ} (hr : r ≠ 0) :
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/Cyclotomic/Discriminant.lean
Original file line number Diff line number Diff line change
Expand Up @@ -109,7 +109,7 @@ theorem discr_prime_pow_ne_two [IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : F
· simp only [H, mul_comm _ (k + 1)]; norm_cast
· have := hne.1
rw [Nat.cast_pow, Ne, pow_eq_zero_iff (by cutsat)] at this
exact absurd (pow_eq_zero h) this
exact absurd (eq_zero_of_pow_eq_zero h) this

/-- If `p` is a prime and `IsCyclotomicExtension {p ^ (k + 1)} K L`, then the discriminant of
`hζ.powerBasis K` is `(-1) ^ (p ^ k * (p - 1) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`
Expand Down
3 changes: 2 additions & 1 deletion Mathlib/NumberTheory/Cyclotomic/PrimitiveRoots.lean
Original file line number Diff line number Diff line change
Expand Up @@ -471,7 +471,8 @@ theorem norm_pow_sub_one_two {k : ℕ} (hζ : IsPrimitiveRoot ζ (2 ^ (k + 1)))
[IsCyclotomicExtension {2 ^ (k + 1)} K L]
(hirr : Irreducible (cyclotomic (2 ^ (k + 1)) K)) :
norm K (ζ ^ 2 ^ k - 1) = (-2 : K) ^ 2 ^ k := by
have := hζ.pow_of_dvd (fun h => two_ne_zero (pow_eq_zero h)) (pow_dvd_pow 2 (le_succ k))
have := hζ.pow_of_dvd
(fun h => two_ne_zero (eq_zero_of_pow_eq_zero h)) (pow_dvd_pow 2 (le_succ k))
rw [Nat.pow_div (le_succ k) zero_lt_two, Nat.succ_sub (le_refl k), Nat.sub_self, pow_one] at this
have H : (-1 : L) - (1 : L) = algebraMap K L (-2) := by
simp only [map_neg, map_ofNat]
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/FLT/Four.lean
Original file line number Diff line number Diff line change
Expand Up @@ -181,7 +181,7 @@ theorem not_minimal {a b c : ℤ} (h : Minimal a b c) (ha2 : a % 2 = 1) (hc : 0
rw [← sq, ht1, (by ring : m ^ 2 - n ^ 2 = m ^ 2 + -n * n)]
exact (Int.isCoprime_iff_gcd_eq_one.mpr ht4).pow_left.add_mul_right_left (-n)
-- m is positive because b is non-zero and b ^ 2 = 2 * m * n and we already have 0 ≤ m.
have hb20 : b ^ 2 ≠ 0 := mt pow_eq_zero h.1.2.1
have hb20 : b ^ 2 ≠ 0 := pow_ne_zero _ h.1.2.1
have h4 : 0 < m := by
apply lt_of_le_of_ne ht6
rintro rfl
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -117,7 +117,7 @@ theorem pow_eq_one_of_norm_eq_one {x : K} (hxi : IsIntegral ℤ x) (hx : ∀ φ
rw [← Nat.sub_add_cancel hlt.le, pow_add, mul_left_eq_self₀] at h
refine h.resolve_right fun hp => ?_
specialize hx (IsAlgClosed.lift (R := ℚ)).toRingHom
rw [pow_eq_zero hp, map_zero, norm_zero] at hx; norm_num at hx
rw [eq_zero_of_pow_eq_zero hp, map_zero, norm_zero] at hx; norm_num at hx

end Bounded

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/NumberTheory/PythagoreanTriples.lean
Original file line number Diff line number Diff line change
Expand Up @@ -435,7 +435,7 @@ theorem isPrimitiveClassified_of_coprime_of_odd_of_pos (hc : Int.gcd x y = 1) (h
have hw1 : w ≠ -1 := by
contrapose! hvz with hw1
rw [hw1, neg_sq, one_pow, add_eq_right] at hq
exact pow_eq_zero hq
exact eq_zero_of_pow_eq_zero hq
have hQ : ∀ x : ℚ, 1 + x ^ 2 ≠ 0 := by
intro q
apply ne_of_gt
Expand Down
4 changes: 2 additions & 2 deletions Mathlib/RingTheory/Coprime/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -402,8 +402,8 @@ theorem sq_add_sq_ne_zero {R : Type*} [CommRing R] [LinearOrder R] [IsStrictOrde
a ^ 2 + b ^ 2 ≠ 0 := by
intro h'
obtain ⟨ha, hb⟩ := (add_eq_zero_iff_of_nonneg (sq_nonneg _) (sq_nonneg _)).mp h'
obtain rfl := pow_eq_zero ha
obtain rfl := pow_eq_zero hb
obtain rfl := eq_zero_of_pow_eq_zero ha
obtain rfl := eq_zero_of_pow_eq_zero hb
exact not_isCoprime_zero_zero h

end IsCoprime
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/DiscreteValuationRing/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -377,7 +377,7 @@ theorem unit_mul_pow_congr_unit {ϖ : R} (hirr : Irreducible ϖ) (u v : Rˣ) (m
rcases h with h | h
· rw [sub_eq_zero] at h
exact mod_cast h
· apply (hirr.ne_zero (pow_eq_zero h)).elim
· apply (hirr.ne_zero (eq_zero_of_pow_eq_zero h)).elim

/-!
## The additive valuation on a DVR
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/Ideal/Operations.lean
Original file line number Diff line number Diff line change
Expand Up @@ -889,7 +889,7 @@ theorem radical_eq_sInf (I : Ideal R) : radical I = sInf { J : Ideal R | I ≤ J
this.radical.symm ▸ (sInf_le ⟨hIm, this⟩ : sInf { J : Ideal R | I ≤ J ∧ IsPrime J } ≤ m) hr

theorem isRadical_bot_of_noZeroDivisors {R} [CommSemiring R] [NoZeroDivisors R] :
(⊥ : Ideal R).IsRadical := fun _ hx => hx.recOn fun _ hn => pow_eq_zero hn
(⊥ : Ideal R).IsRadical := fun _ hx => hx.recOn fun _ hn => eq_zero_of_pow_eq_zero hn

@[simp]
theorem radical_bot_of_noZeroDivisors {R : Type u} [CommSemiring R] [NoZeroDivisors R] :
Expand Down
5 changes: 3 additions & 2 deletions Mathlib/RingTheory/Jacobson/Ring.lean
Original file line number Diff line number Diff line change
Expand Up @@ -447,7 +447,7 @@ theorem isMaximal_comap_C_of_isMaximal [IsJacobsonRing R] [Nontrivial R]
fun x hx => by
rwa [Quotient.eq_zero_iff_mem, (by rwa [eq_bot_iff] : (P.comap C : Ideal R) = ⊥)] at hx)
(by simpa only [a, leadingCoeff_eq_zero, Polynomial.map_zero] using hp0')
have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ => hp0 (pow_eq_zero hn)
have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ => hp0 (eq_zero_of_pow_eq_zero hn)
suffices (⊥ : Ideal (Localization M)).IsMaximal by
rw [← IsLocalization.comap_map_of_isPrime_disjoint M (Localization M) ⊥ bot_prime
(disjoint_iff_inf_le.mpr fun x hx => hM (hx.2 ▸ hx.1))]
Expand Down Expand Up @@ -483,7 +483,8 @@ private theorem quotient_mk_comp_C_isIntegral_of_jacobson' [Nontrivial R] (hR :
let M : Submonoid (R ⧸ P') := Submonoid.powers a
let φ : R ⧸ P' →+* R[X] ⧸ P := quotientMap P C le_rfl
have hP'_prime : P'.IsPrime := comap_isPrime C P
have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ => hp0 <| leadingCoeff_eq_zero.mp (pow_eq_zero hn)
have hM : (0 : R ⧸ P') ∉ M := fun ⟨n, hn⟩ =>
hp0 <| leadingCoeff_eq_zero.mp (eq_zero_of_pow_eq_zero hn)
let M' : Submonoid (R[X] ⧸ P) := M.map φ
refine RingHom.IsIntegral.tower_bot φ (algebraMap _ (Localization M')) ?_ ?_
· refine IsLocalization.injective (Localization M')
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/Nilpotent/Defs.lean
Original file line number Diff line number Diff line change
Expand Up @@ -193,7 +193,7 @@ end IsReduced

instance (priority := 900) isReduced_of_noZeroDivisors [MonoidWithZero R] [NoZeroDivisors R] :
IsReduced R :=
⟨fun _ ⟨_, hn⟩ => pow_eq_zero hn⟩
⟨fun _ ⟨_, hn⟩ => eq_zero_of_pow_eq_zero hn⟩

instance (priority := 900) isReduced_of_subsingleton [Zero R] [Pow R ℕ] [Subsingleton R] :
IsReduced R :=
Expand Down
4 changes: 3 additions & 1 deletion Mathlib/RingTheory/Perfection.lean
Original file line number Diff line number Diff line change
Expand Up @@ -568,7 +568,9 @@ theorem map_eq_zero {f : PreTilt O p} : val K v O hv p f = 0 ↔ f = 0 := by
· rw [hf0]; exact iff_of_true (Valuation.map_zero _) rfl
obtain ⟨n, hn⟩ : ∃ n, coeff _ _ n f ≠ 0 := not_forall.1 fun h => hf0 <| Perfection.ext h
change valAux K v O p f = 0 ↔ f = 0; refine iff_of_false (fun hvf => hn ?_) hf0
rw [valAux_eq hv hn] at hvf; replace hvf := pow_eq_zero hvf; rwa [ModP.preVal_eq_zero hv] at hvf
rw [valAux_eq hv hn] at hvf
replace hvf := eq_zero_of_pow_eq_zero hvf
rwa [ModP.preVal_eq_zero hv] at hvf

end Classical

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/Polynomial/Cyclotomic/Expand.lean
Original file line number Diff line number Diff line change
Expand Up @@ -172,7 +172,7 @@ theorem isRoot_cyclotomic_prime_pow_mul_iff_of_charP {m k p : ℕ} {R : Type*} [
refine ⟨fun h => ?_, fun h => ?_⟩
· rw [IsRoot.def, cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, eval_pow]
at h
replace h := pow_eq_zero h
replace h := eq_zero_of_pow_eq_zero h
rwa [← IsRoot.def, isRoot_cyclotomic_iff] at h
· rw [← isRoot_cyclotomic_iff, IsRoot.def] at h
rw [cyclotomic_mul_prime_pow_eq R (NeZero.not_char_dvd R p m) hk, IsRoot.def, eval_pow,
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/RingTheory/Polynomial/Selmer.lean
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ theorem X_pow_sub_X_sub_one_irreducible_aux (z : ℂ) : ¬(z ^ n = z + 1 ∧ z ^
rcases key with (key | key | key)
· exact z_ne_zero (by rwa [key, right_eq_add] at h1)
· exact one_ne_zero (by rwa [key, left_eq_add] at h1)
· exact z_ne_zero (pow_eq_zero (by rwa [key, add_self_eq_zero] at h2))
· exact z_ne_zero (eq_zero_of_pow_eq_zero (by rwa [key, add_self_eq_zero] at h2))

theorem X_pow_sub_X_sub_one_irreducible (hn1 : n ≠ 1) : Irreducible (X ^ n - X - 1 : ℤ[X]) := by
by_cases hn0 : n = 0
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/LinearCombination'.lean
Original file line number Diff line number Diff line change
Expand Up @@ -128,7 +128,7 @@ theorem eq_of_add [AddGroup α] (p : (a : α) = b) (H : (a' - b') - (a - b) = 0)

theorem eq_of_add_pow [Ring α] [NoZeroDivisors α] (n : ℕ) (p : (a : α) = b)
(H : (a' - b') ^ n - (a - b) = 0) : a' = b' := by
rw [← sub_eq_zero] at p ⊢; apply pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H
rw [← sub_eq_zero] at p ⊢; apply eq_zero_of_pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H

/-- Implementation of `linear_combination'` and `linear_combination2`. -/
def elabLinearCombination' (tk : Syntax)
Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Tactic/LinearCombination/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -190,7 +190,7 @@ theorem lt_rearrange {α : Type*} [AddCommGroup α] [PartialOrder α] [IsOrdered

theorem eq_of_add_pow [Ring α] [NoZeroDivisors α] (n : ℕ) (p : (a : α) = b)
(H : (a' - b') ^ n - (a - b) = 0) : a' = b' := by
rw [← sub_eq_zero] at p ⊢; apply pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H
rw [← sub_eq_zero] at p ⊢; apply eq_zero_of_pow_eq_zero (n := n); rwa [sub_eq_zero, p] at H

end Tactic.LinearCombination

Expand Down
2 changes: 1 addition & 1 deletion Mathlib/Topology/Instances/ENNReal/Lemmas.lean
Original file line number Diff line number Diff line change
Expand Up @@ -405,7 +405,7 @@ protected theorem continuous_pow (n : ℕ) : Continuous fun a : ℝ≥0∞ => a
intro x
refine ENNReal.Tendsto.mul (IH.tendsto _) ?_ tendsto_id ?_ <;> by_cases H : x = 0
· simp only [H, zero_ne_top, Ne, or_true, not_false_iff]
· exact Or.inl fun h => H (pow_eq_zero h)
· exact Or.inl fun h => H (eq_zero_of_pow_eq_zero h)
· simp only [H, pow_eq_top_iff, zero_ne_top, false_or, not_true, Ne,
not_false_iff, false_and]
· simp only [H, true_or, Ne, not_false_iff]
Expand Down