zeroLocus_smul_of_isUnit — Mathlib

English

If r is a unit in R, then multiplying a set by r does not change its zero locus:

Русский

Если r — единица в R, умножение множества на r не изменяет нулевой локус:

LaTeX

$$$\\mathrm{zeroLocus}(r \\cdot s) = \\mathrm{zeroLocus}(s) \\quad \\text{if } r \\text{ is a unit}.$$$

Lean4

theorem zeroLocus_smul_of_isUnit {r : R} (hr : IsUnit r) (s : Set R) : zeroLocus (r • s) = zeroLocus s := by ext;
  simp [Set.subset_def, ← Set.image_smul, Ideal.unit_mul_mem_iff_mem _ hr]

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