exists_mul_eq_one — Mathlib

English

In a finite-dimensional F-K algebra K over a field F that is an integral domain, every nonzero element x ∈ K has a multiplicative inverse.

Русский

В конечномерной алгебре над полем F, если K является интегральным доменом, то каждый ненулевой элемент x ∈ K имеет обратный элемент относительно умножения.

LaTeX

$$$\forall x\in K,\, x \neq 0 \Rightarrow \exists y\in K,\, x\,y = 1$$$

Lean4

theorem exists_mul_eq_one (F : Type*) {K : Type*} [Field F] [Ring K] [IsDomain K] [Algebra F K] [FiniteDimensional F K]
    {x : K} (H : x ≠ 0) : ∃ y, x * y = 1 :=
  by
  have : Function.Surjective (LinearMap.mulLeft F x) :=
    LinearMap.injective_iff_surjective.1 fun y z => ((mul_right_inj' H).1 : x * y = x * z → y = z)
  exact this 1

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