extendScalarsOfSurjective_symm — Mathlib

English

The symmetry relation for extendScalarsOfSurjective is preserved under evaluation: (f.extendScalarsOfSurjective h).symm x = (f.symm.extendScalarsOfSurjective h) x.

Русский

Симметричная связь сохраняется при применении к элементу: (f.extendScalarsOfSurjective h).symm x = (f.symm.extendScalarsOfSurjective h) x.

LaTeX

$$$\\big( f.extendScalarsOfSurjective\\; h \\big)^{-1}(x) = f^{-1}(x)$$$

Lean4

@[simp]
theorem extendScalarsOfSurjective_symm (f : M ≃ₗ[R] N) :
    (f.extendScalarsOfSurjective h).symm = f.symm.extendScalarsOfSurjective h :=
  rfl

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