Commit 2026-08-18 10:14 1acd7e04
View on Github →chore(Data/Nat/Prime): privatize theorems about minFacProp (#42870)
minFacProp is a helper def to prove some properties about minFac, but not useful on its own (this is why its private in the first place). The helper lemmas for minFacProp are similar and should therefore also be private.