num_zero_eq — Mathlib

English

If the map algebraMap R P is injective, then the numerator of the zero fractional ideal is zero.

Русский

Если отображение алгебраического отображения инъективно, то числитель нулевого дробного идеала равен нулю.

LaTeX

$$$\text{num}(0) = 0$ (assuming injectivity of $\mathrm{algebraMap}$)$$

Lean4

theorem num_zero_eq (h_inj : Function.Injective (algebraMap R P)) : num (0 : FractionalIdeal S P) = 0 := by
  simpa [num, LinearMap.ker_eq_bot] using h_inj

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