associatesEquivIsPrincipal_map_zero

English

The image of the zero associate under the equivalence is the zero principal ideal.

Русский

Образ нулевого ассоциата при эквивалентности равен нулевому главному идеалу.

LaTeX

$$$(associatesEquivIsPrincipal \; R\; 0) = 0$$$

Lean4

@[simp]
theorem associatesEquivIsPrincipal_map_zero : (associatesEquivIsPrincipal R 0 : Ideal R) = 0 := by
  rw [← mk_zero, associatesEquivIsPrincipal_apply, Submodule.zero_eq_bot, span_singleton_eq_bot]

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