range

Mathlib.Algebra.Module.Submodule.Equiv

URI: https://scilib.ai/kg/mathlib#LinearEquiv.range

English

For a linear equivalence e, the range is the whole target space.

Русский

Для линейной эквивалентности e образ равен всей целевой области.

LaTeX

$$protected theorem range : LinearMap.range (e : M →ₛₗ[σ₁₂] M₂) = ⊤$$

Lean4

@[simp]
protected theorem range : LinearMap.range (e : M →ₛₗ[σ₁₂] M₂) = ⊤ :=
  LinearMap.range_eq_top.2 e.toEquiv.surjective

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

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

Разделы

Аффилиация

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