spanSingleton_eq_spanSingleton — Mathlib

English

Two spans are equal iff they are generated by a unit multiple; equivalently, I = spanSingleton S x for some x.

Русский

Два порождения равны тогда и только тогда, когда они порождены единицей на x; то есть I = spanSingleton S x.

LaTeX

$$$ I = \operatorname{spanSingleton} S x \iff \exists x', I = \operatorname{spanSingleton} S x' $$$

Lean4

theorem spanSingleton_eq_spanSingleton [NoZeroSMulDivisors R P] {x y : P} :
    spanSingleton S x = spanSingleton S y ↔ ∃ z : Rˣ, z • x = y :=
  by
  rw [← Submodule.span_singleton_eq_span_singleton, spanSingleton, spanSingleton]
  exact Subtype.mk_eq_mk

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