addVal_eq_top_iff — Mathlib

English

For any x, addVal(x) = ⊤ if and only if x = 0.

Русский

Для любого x: addVal(x) = ⊤ тогда и только тогда, когда x = 0.

LaTeX

$$$\mathrm{addVal}(x) = \top \iff x = 0$$$

Lean4

theorem addVal_eq_top_iff {a : R} : addVal R a = ⊤ ↔ a = 0 :=
  by
  have hi := (Classical.choose_spec (exists_prime R)).irreducible
  constructor
  · contrapose
    intro h
    obtain ⟨n, ha⟩ := associated_pow_irreducible h hi
    obtain ⟨u, rfl⟩ := ha.symm
    rw [mul_comm, addVal_def' u hi n]
    nofun
  · rintro rfl
    exact addVal_zero

Похожие утверждения