basis — Mathlib

English

Same as above: the inverse maps specify the two coordinates as a pair.

Русский

То же самое: обратное отображение задаёт две координаты пары.

LaTeX

$$$ (\\text{linearEquivTuple } a b)^{-1} x = \\langle x_0, x_1 \\rangle $$$

Lean4

/-- `QuadraticAlgebra R a b` has a basis over `R` given by `1` and `i` -/
noncomputable def basis : Module.Basis (Fin 2) R (QuadraticAlgebra R a b) :=
  .ofEquivFun <| linearEquivTuple a b

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