invertibleιOfInvertible — Mathlib

English

If two-sided data ensure that Q(m) is invertible, then the Clifford embedding ι_Q(m) is also invertible in the appropriate endomorphism ring, given a fixed even/odd grading.

Русский

Если простые данные обеспечивают обратимость Q(m), тогда вложение ι_Q(m) также обратимо в соответствующем кольце эндоморфизмов, при заданной градации.

LaTeX

$$invertibleιOfInvertible(Q,m)$$

Lean4

/-- If the quadratic form of a vector is invertible, then so is that vector. -/
def invertibleιOfInvertible (m : M) [Invertible (Q m)] : Invertible (ι Q m)
    where
  invOf := ι Q (⅟(Q m) • m)
  invOf_mul_self := by rw [map_smul, smul_mul_assoc, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]
  mul_invOf_self := by rw [map_smul, mul_smul_comm, ι_sq_scalar, Algebra.smul_def, ← map_mul, invOf_mul_self, map_one]

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