of_h_eq_floor — Mathlib

English

The head term h of (of v) is the cast of the floor of v, i.e., h = ⌊v⌋ cast into the ambient ring.

Русский

Головной член h продолжающей дроби равен приводке ⌊v⌋ к исходной структуре: h = ⌊v⌋.cast.

LaTeX

$$$(\operatorname{of} v).h = (\lfloor v \rfloor)^{\mathrm{cast}}$$$

Lean4

/-- The head term of the gcf of `v` is `⌊v⌋`. -/
@[simp]
theorem of_h_eq_floor : (of v).h = ⌊v⌋ := by simp [of_h_eq_intFractPair_seq1_fst_b, IntFractPair.of]

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