areaForm_comp_linearIsometryEquiv

English

The map sending x,y in F via φ to areaForm in E equals the areaForm in E with arguments pulled back by φ.

Русский

Отображение, переносимое через φ, сохраняет площадь через вытягивание аргументов обратно.

LaTeX

$$AreaForm(φ x, φ y) = AreaForm_E(φ^{-1}x, φ^{-1}y)$$

Lean4

/-- The area form is invariant under pullback by a positively-oriented isometric automorphism. -/
theorem areaForm_comp_linearIsometryEquiv (φ : E ≃ₗᵢ[ℝ] E) (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E))
    (x y : E) : o.areaForm (φ x) (φ y) = o.areaForm x y :=
  by
  convert o.areaForm_map φ (φ x) (φ y)
  · symm
    rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ
    rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin]
  · simp
  · simp

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