range_le_bot_iff

Mathlib.Algebra.Module.Submodule.Range

URI: https://scilib.ai/kg/mathlib#LinearMap.range_le_bot_iff

English

The range of a semilinear map is bottom if and only if the map is zero.

Русский

Диапазон семилинейного отображения равен нулю тогда и только тогда, когда отображение равно нулю.

LaTeX

$$$\operatorname{range} f = \bot \iff f = 0$$$

Lean4

theorem range_le_bot_iff (f : M →ₛₗ[τ₁₂] M₂) : range f ≤ ⊥ ↔ f = 0 := by rw [range_le_iff_comap]; exact ker_eq_top

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

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

Разделы

Аффилиация

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