Commit 2023-09-15 04:33 f80bb2fb
View on Github →feat: Finsets of cardinality > 1 in Pi types (#6818)
Add an equivalent condition for 1 < m * n in Nat, and two lemmas about Finsets of cardinality > 1.
feat: Finsets of cardinality > 1 in Pi types (#6818)
Add an equivalent condition for 1 < m * n in Nat, and two lemmas about Finsets of cardinality > 1.