Transport the property by positive multiplication
ProvedErdosStraus242.scalingegyptian-fractionsnumber-theory
For natural numbers , if has three distinct positive ordered denominators representing and , then has such a decomposition.
Preamble
import Definitions.Def_ErdosStraus242 import Mathlib.Data.Nat.Prime.Basic import Mathlib.Data.Finset.Insert
Formal statement
namespace ErdosStraus242
theorem scaling (n k : ℕ) (h : IsErdosStraus n) (hk : 0 < k) :
IsErdosStraus (k*n) := by sorry
end ErdosStraus242
Source
Bloom–Elsholtz (2022), p. 239, https://www.math.tugraz.at/~elsholtz/WWW/papers/bloom-elsholtz-naw5-2022-23-4-237.pdf; witness refinement in scale_witness.
Read-back
What the Lean code literally says, in plain math · Codex GPT-6 (independent fresh-context sub-agent)
For every pair of natural numbers and , if and there exist natural numbers such that , , , and , then there exist natural numbers such that , , , and . Every fraction and each equality here is interpreted in the rational numbers, with the natural numbers in it viewed as rational numbers. The quantification over includes ; in that case rational division gives , whereas the three positive reciprocal terms in the hypothesis have a positive sum, so the hypothesis cannot hold. The assumption excludes .
Human review
Confirmed by the mission captain (proposal self-audit).