map_eq_zero_iff

Mathlib.Topology.Algebra.Module.Equiv

URI: https://scilib.ai/kg/mathlib#ContinuousLinearEquiv.map_eq_zero_iff

English

If two continuous linear equivalences agree at the unit, then they are equal: f(1) = g(1) implies f = g.

Русский

Если две непрерывные линейные эквивалентности совпадают в единице, то они равны: f(1) = g(1) ⇒ f = g.

LaTeX

$$$f(1) = g(1) \Rightarrow f = g$$$

Lean4

theorem map_eq_zero_iff (e : M₁ ≃SL[σ₁₂] M₂) {x : M₁} : e x = 0 ↔ x = 0 :=
  e.toLinearEquiv.map_eq_zero_iff

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

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

Разделы

Аффилиация

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