const_ext — Mathlib

English

If f1 g2 = f2 g1, then const_R f1 g1 U hu1 equals const_R f2 g2 U hu2. This is a refinement of const that relates two representations of the same local fraction.

Русский

Если f1 g2 = f2 g1, то const_R f1 g1 равняется const_R f2 g2, на соответствующих открытых.

LaTeX

$$$ f_1 g_2 = f_2 g_1 \\Rightarrow const_R f_1 g_1 U hu_1 = const_R f_2 g_2 U hu_2 $$$

Lean4

theorem const_ext {f₁ f₂ g₁ g₂ : R} {U hu₁ hu₂} (h : f₁ * g₂ = f₂ * g₁) : const R f₁ g₁ U hu₁ = const R f₂ g₂ U hu₂ :=
  Subtype.eq <|
    funext fun x => IsLocalization.mk'_eq_of_eq (by rw [mul_comm, Subtype.coe_mk, ← h, mul_comm, Subtype.coe_mk])

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