dual_injective — Mathlib

English

The image of the different ideal under the natural coeSubmodule map from FractionRing B equals the inverse of Submodule traceDual at 1.

Русский

Образ различного идеала через естественный отображатель coeSubmodule соответствует обратному traceDual в 1.

LaTeX

$$\mathrm{coeSubmodule}_{\FractionRing B}(\mathrm{differentIdeal}(A,B)) = (\mathrm{Submodule.traceDual}(A, \FractionRing A, 1))^{-1}$$

Lean4

theorem dual_injective : Function.Injective (dual A K : FractionalIdeal B⁰ L → FractionalIdeal B⁰ L) :=
  dual_involutive.injective

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