lean_workbook_plus_14827

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

$\frac{y_A}{x_A}=7$ then $y_A= 7x_A$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14827 (x_A y_A : ℝ) (h : y_A / x_A = 7) : y_A = 7 * x_A   :=  by sorry

Source