const_congr — Mathlib

English

If f1 = f2 then const_R f1 g1 U hu1 equals const_R f2 g2 U hu2 provided g1 = g2; this is the congruence of constants under identical numerators and denominators.

Русский

Если f1 = f2 и g1 = g2, то const_R f1 g1 = const_R f2 g2; константы совпадают при равенстве числителя и знаменателя.

LaTeX

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

Lean4

theorem const_congr {f₁ f₂ g₁ g₂ : R} {U hu} (hf : f₁ = f₂) (hg : g₁ = g₂) :
    const R f₁ g₁ U hu = const R f₂ g₂ U (hg ▸ hu) := by substs hf hg; rfl

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