English
If f respects hf and hd, then lift preserves multiplication: lift f hf (a*b) = lift f hf a · lift f hf b.
Русский
Если f удовлетворяет hf и hd инициализирует, то лифтинг сохраняет умножение: L(a b) = L(a) L(b).
LaTeX
$$$\text{ValueGroupWithZero.lift}(f,hf)(a\cdot b) = \text{ValueGroupWithZero.lift}(f,hf)(a) \; \cdot \; \text{ValueGroupWithZero.lift}(f,hf)(b)$$$
Lean4
theorem lift_mul {α : Type*} [Mul α] (f : R → posSubmonoid R → α)
(hf : ∀ (x y : R) (t s : posSubmonoid R), x * t ≤ᵥ y * s → y * s ≤ᵥ x * t → f x s = f y t)
(hdist : ∀ (a b r s), f (a * b) (r * s) = f a r * f b s) (a b : ValueGroupWithZero R) :
ValueGroupWithZero.lift f hf (a * b) = ValueGroupWithZero.lift f hf a * ValueGroupWithZero.lift f hf b :=
by
induction a using ValueGroupWithZero.ind
induction b using ValueGroupWithZero.ind
simpa using hdist _ _ _ _
