English
If x ≠ 0 in ModP O p, then x^p ≠ 0 in ModP O p.
Русский
Если x ≠ 0 в ModP O p, то x^p ≠ 0 в ModP O p.
LaTeX
$$$x \neq 0 \Rightarrow x^p \neq 0$ in ModP O p$$
Lean4
theorem mul_ne_zero_of_pow_p_ne_zero {x y : ModP O p} (hx : x ^ p ≠ 0) (hy : y ^ p ≠ 0) : x * y ≠ 0 :=
by
obtain ⟨r, rfl⟩ := Ideal.Quotient.mk_surjective x
obtain ⟨s, rfl⟩ := Ideal.Quotient.mk_surjective y
have h1p : (0 : ℝ) < 1 / p := one_div_pos.2 (Nat.cast_pos.2 hp.1.pos)
rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_mul]
rw [← (Ideal.Quotient.mk (Ideal.span {(p : O)})).map_pow] at hx hy
rw [← v_p_lt_val hv] at hx hy ⊢
rw [RingHom.map_pow, v.map_pow, ← rpow_lt_rpow_iff h1p, ← rpow_natCast, ← rpow_mul,
mul_one_div_cancel (Nat.cast_ne_zero.2 hp.1.ne_zero : (p : ℝ) ≠ 0), rpow_one] at hx hy
rw [RingHom.map_mul, v.map_mul]; refine lt_of_le_of_lt ?_ (mul_lt_mul'' hx hy zero_le' zero_le')
by_cases hvp : v p = 0
· rw [hvp]; exact zero_le _
replace hvp := zero_lt_iff.2 hvp
conv_lhs => rw [← rpow_one (v p)]
rw [← rpow_add (ne_of_gt hvp)]
refine rpow_le_rpow_of_exponent_ge hvp (map_natCast (algebraMap O K) p ▸ hv.2 _) ?_
rw [← add_div, div_le_one (Nat.cast_pos.2 hp.1.pos : 0 < (p : ℝ))]; exact mod_cast hp.1.two_le
