exists_inv — Mathlib

English

For the i-th component, if its image is zero in the limit, then there exists a larger stage where the image is zero in that stage.

Русский

Для i-й компоненты, если её образ равен нулю в пределе, существует больший этап, на котором образ равен нулю на этом этапе.

LaTeX

$$$\\forall i, \\exists j \\ge i, f'_{i j}(x) = 0.$$$

Lean4

theorem exists_inv {p : Ring.DirectLimit G f} : p ≠ 0 → ∃ y, p * y = 1 :=
  Ring.DirectLimit.induction_on p fun i x H ↦
    ⟨Ring.DirectLimit.of G f i x⁻¹, by
      rw [← (Ring.DirectLimit.of _ _ _).map_mul,
        mul_inv_cancel₀ fun h : x = 0 ↦ H <| by rw [h, (Ring.DirectLimit.of _ _ _).map_zero],
        (Ring.DirectLimit.of _ _ _).map_one]⟩

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