Theorem Nat.factorization_one_right

Modification history

2025-07-05 07:48

Mathlib/Data/Nat/Factorization/Basic.lean

chore(Data/Nat/Factorization/Basic): minimize dependencies (#24330)

Modified Nat.factorization_one_right View on Github →

2023-03-28 12:18

Mathlib/Data/Nat/Factorization/Basic.lean

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

Added Nat.factorization_one_right View on Github →