ratioHom — Mathlib

English

The inverse of ratio equals the ratio of the inverse, i.e., ratio(e^{-1}) = (ratio e)^{-1}.

Русский

Обратное значение ratio равно обратному ratio.

LaTeX

$$$\operatorname{ratio}(e^{-1}) = (\operatorname{ratio}(e))^{-1}$$$

Lean4

/-- `Dilation.ratio` as a monoid homomorphism. -/
noncomputable def ratioHom : (X ≃ᵈ X) →* ℝ≥0 where
  toFun := Dilation.ratio
  map_one' := ratio_refl
  map_mul' _ _ := (ratio_trans _ _).trans (mul_comm _ _)

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