congrQuadraticMap_refl — Mathlib

English

The identity linear equivalence yields the identity on the space of quadratic maps: congrQuadraticMap of a reflection is the reflection on QuadraticMap space.

Русский

Идентичное линейное эквивалентное отображение дает тождественное отображение на пространстве квадратичных отображений.

LaTeX

$$$\text{congrQuadraticMap} (\mathrm{refl}\, R\, N) = \mathrm{refl}\, R\, (QuadraticMap\, R\, M\, N).$$$

Lean4

@[simp]
theorem _root_.LinearEquiv.congrQuadraticMap_refl :
    LinearEquiv.congrQuadraticMap (.refl R N) = .refl R (QuadraticMap R M N) :=
  rfl

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