extendScalarsOfSurjective_apply — Mathlib

English

For surjective algebraMap, the inverse of the extension is the extension of the inverse: (f.extendScalarsOfSurjective h).symm = f.symm.extendScalarsOfSurjective h.

Русский

Если отображение алгебраMap сюръективно, то обратное расширения скаляров равно расширению обратного: (f.extendScalarsOfSurjective h).symm = f.symm.extendScalarsOfSurjective h.

LaTeX

$$$\\big( f.extendScalarsOfSurjective\\; h \\big).symm = f.symm.extendScalarsOfSurjective h$$$

Lean4

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

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