mul_inv — Mathlib

English

An element is not a unit if and only if its norm is less than 1.

Русский

Элемент не является единицей тогда и только тогда, когда его норма меньше 1.

LaTeX

$$¬\mathrm{IsUnit}(z) \iff \|z\| < 1$$

Lean4

theorem mul_inv : ∀ {z : ℤ_[p]}, ‖z‖ = 1 → z * z.inv = 1
  | ⟨k, _⟩, h => by
    have hk : k ≠ 0 := fun h' => zero_ne_one' ℚ_[p] (by simp [h'] at h)
    unfold PadicInt.inv
    rw [norm_eq_padic_norm] at h
    dsimp only
    rw [dif_pos h]
    apply Subtype.ext_iff.2
    simp [mul_inv_cancel₀ hk]

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