invertibleOfInvertibleι — Mathlib

English

Over rings with 2 invertible, invertibility of ι_Q(m) implies invertibility of Q(m) within the exterior-algebraic viewpoint linking the two maps.

Русский

В кольце, где 2 обратим, обратимость ι_Q(m) влечёт обратимость Q(m) через соответствие карты в экстериорной алгебре.

LaTeX

$$invertibleOfInvertibleι(Q,m)$$

Lean4

/-- Over a ring where `2` is invertible, `Q m` is invertible whenever `ι Q m`. -/
def invertibleOfInvertibleι (m : M) [Invertible (ι Q m)] : Invertible (Q m) :=
  ExteriorAlgebra.invertibleAlgebraMapEquiv M (Q m) <|
    .algebraMapOfInvertibleAlgebraMap (equivExterior Q).toLinearMap (by simp) <|
      .copy (.mul ‹Invertible (ι Q m)› ‹Invertible (ι Q m)›) _ (ι_sq_scalar _ _).symm

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