map_apply — Mathlib

English

The application of the induced map to a nonzero alternating map has a precise formula.

Русский

Применение соответствующего отображения к ненулевому чередующему отображению задается точной формулой.

LaTeX

$$$\text{map_apply}: \; Orientation.map ι e (rayOfNeZero _ v hv) = \text{rayOfNeZero} _ (v.compLinearMap e.symm) (mt (v.compLinearEquiv_eq_zero_iff e.symm).mp hv).$$$

Lean4

@[simp]
theorem map_apply (e : M ≃ₗ[R] N) (v : M [⋀^ι]→ₗ[R] R) (hv : v ≠ 0) :
    Orientation.map ι e (rayOfNeZero _ v hv) =
      rayOfNeZero _ (v.compLinearMap e.symm) (mt (v.compLinearEquiv_eq_zero_iff e.symm).mp hv) :=
  rfl

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