den_mul_self_eq_num — Mathlib

English

One has the equality of the fractional operations: I.den • I = Submodule.map (Algebra.linearMap R P) I.num.

Русский

Справедливо равенство операций дробных: I.den • I = map(Algebra.linearMap) I.num.

LaTeX

$$$I.den \\cdot I = Submodule.map(\\mathsf{Algebra.linearMap}\\,R\\,P)(I.num)$$$

Lean4

theorem den_mul_self_eq_num (I : FractionalIdeal S P) :
    I.den • (I : Submodule R P) = Submodule.map (Algebra.linearMap R P) I.num :=
  by
  rw [den, num, Submodule.map_comap_eq]
  refine (inf_of_le_right ?_).symm
  rintro _ ⟨a, ha, rfl⟩
  exact I.2.choose_spec.2 a ha

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