ratio_symm — Mathlib

English

The ratio of a composition e.trans e' equals the product of their ratios.

Русский

Отношение дилатаций в композиции равно произведению их отношении.

LaTeX

$$$\operatorname{ratio}(e \; \mathrm{trans}\; e') = \operatorname{ratio}(e) \cdot \operatorname{ratio}(e')$$$

Lean4

@[simp]
theorem ratio_symm (e : X ≃ᵈ Y) : ratio e.symm = (ratio e)⁻¹ :=
  eq_inv_of_mul_eq_one_left <| by rw [← ratio_trans, symm_trans_self, ratio_refl]

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