eq_algebraMap_or_inv_eq_algebraMap

English

For any x in F there exists a in O with either x = φ(a) or x^{-1} = φ(a).

Русский

Для любого x в F существует a ∈ O такой, что x = φ(a) или x^{-1} = φ(a).

LaTeX

$$$\exists a \in O,\ x = \mathrm{algebraMap}(O,F)(a) \ \text{или}\ x^{-1} = \mathrm{algebraMap}(O,F)(a)$$$

Lean4

theorem eq_algebraMap_or_inv_eq_algebraMap (hv : Integers v O) (x : F) :
    ∃ a : O, x = algebraMap O F a ∨ x⁻¹ = algebraMap O F a :=
  by
  rcases val_le_one_or_val_inv_le_one v x with h | h <;> obtain ⟨a, ha⟩ := exists_of_le_one hv h
  exacts [⟨a, Or.inl ha.symm⟩, ⟨a, Or.inr ha.symm⟩]

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