coe_div — Mathlib

English

For U1, U2 ∈ unitary R, the quotient in the subtype maps to the quotient in R: the inclusion preserves division.

Русский

Для U1, U2 ∈ unitary R частное в подтипе переходит в частное в R: вложение сохраняет деление.

LaTeX

$$$\uparrow\left(\frac{U_1}{U_2}\right) = \frac{\uparrow U_1}{\uparrow U_2}$$$

Lean4

@[norm_cast]
theorem coe_div (U₁ U₂ : unitary R) : ↑(U₁ / U₂) = (U₁ / U₂ : R) := by
  simp only [div_eq_mul_inv, coe_inv, Submonoid.coe_mul]

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