ext'

Mathlib.LinearAlgebra.LinearPMap

URI: https://scilib.ai/kg/mathlib#LinearPMap.ext'

English

A variant of ext allowing equality under a prescribed equality of inputs.

Русский

Вариант ext с допуском равенства входов по заданному равенству.

LaTeX

$$$$f = g \Rightarrow \text{ext' } f g.$$$$

Lean4

theorem ext' {s : Submodule R E} {f g : s →ₗ[R] F} (h : f = g) : mk s f = mk s g :=
  h ▸ rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru