Quotient_of_Homogeneous_Functions
Provedanalysishomogeneous-functionsproofwiki
The quotient of two homogeneous functions of the same degree is homogeneous of degree 0.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Quotient_of_Homogeneous_Functions (M N : ℝ → ℝ → ℝ) (n : ℕ) (hM : ∀ t x y, M (t * x) (t * y) = t ^ n * M x y) (hN : ∀ t x y, N (t * x) (t * y) = t ^ n * N x y) (x y : ℝ) (hN0 : N x y ≠ 0) (hNy : N 1 (y / x) ≠ 0) (hx : x ≠ 0) : M x y / N x y = M 1 (y / x) / N 1 (y / x) := by sorry
Source