div_one — Mathlib

English

Dividing a fractional ideal by the unit fractional ideal leaves it unchanged: I / 1 = I.

Русский

Деление дробного идеала на единичный дробный идеал оставляет его неизменным: I / 1 = I.

LaTeX

$$$ I / 1 = I $$$

Lean4

@[simp]
theorem div_one {I : FractionalIdeal R₁⁰ K} : I / 1 = I :=
  by
  rw [div_nonzero (one_ne_zero' (FractionalIdeal R₁⁰ K))]
  ext
  constructor <;> intro h
  · simpa using mem_div_iff_forall_mul_mem.mp h 1 ((algebraMap R₁ K).map_one ▸ coe_mem_one R₁⁰ 1)
  · apply mem_div_iff_forall_mul_mem.mpr
    rintro y ⟨y', _, rfl⟩
    convert Submodule.smul_mem _ y' h using 1
    rw [mul_comm, Algebra.linearMap_apply, ← Algebra.smul_def]

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