cons_mem_invSet — Mathlib

English

If a' ≠ 0 and a' < a and b ∈ invSet(a), then invAux(a') · (1 + (a + a') · b) ∈ invSet(a).

Русский

Если a' ≠ 0 и a' < a и b ∈ invSet(a), то invAux(a') · (1 + (a + a') · b) ∈ invSet(a).

LaTeX

$$$ a' \neq 0 \land a' < a \land b \in invSet(a) \Rightarrow invAux(a') \cdot (1 + (a + a') \cdot b) \in invSet(a)$$$

Lean4

/-- "cons" is our operation `(1 + (a + a') * b) / a'` in the definition of the inverse. -/
theorem cons_mem_invSet {a' : Nimber} (ha₀ : a' ≠ 0) (ha : a' < a) (hb : b ∈ invSet a) :
    invAux a' * (1 + (a + a') * b) ∈ invSet a := by
  rw [invSet] at hb ⊢
  exact Set.mem_sInter.2 fun _ hs => hs.2 _ ha ha₀ _ (Set.mem_sInter.1 hb _ hs)

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