Theorem Nat.ord_compl_of_not_prime

Modification history

2024-11-03 19:16

Mathlib/Data/Nat/Factorization/Basic.lean

chore(Nat.Factorization): rename `ord_proj/compl` -> `ordProj/Compl` (#18191) …

Deleted Nat.ord_compl_of_not_prime View on Github →

2023-03-28 12:18

Mathlib/Data/Nat/Factorization/Basic.lean

feat: Port/Data.Nat.Factorization.Basic (#3043)

Added Nat.ord_compl_of_not_prime View on Github →