num_zero — Mathlib

English

The numerator of 0 is 0.

Русский

Числитель нуля равен нулю.

LaTeX

$$$\\mathrm{num}_A(0) = 0$$$

Lean4

@[simp]
theorem num_zero : IsFractionRing.num A (0 : K) = 0 :=
  by
  have := mk'_num_den' A (0 : K)
  simp only [div_eq_zero_iff] at this
  rcases this with h | h
  · exact FaithfulSMul.algebraMap_injective A K (by convert h; simp)
  · replace h : algebraMap A K (den A (0 : K)) = algebraMap A K 0 := by convert h; simp
    absurd FaithfulSMul.algebraMap_injective A K h
    apply nonZeroDivisors.coe_ne_zero

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