Commit 2022-08-10 05:50 36d300ce

View on Github →

refactor(data/fintype/basic): drop 2 noncomputable instances (#15943) Drop fintype.of_subsingleton' and function.embedding.fintype'. First, we should use finite instances instead of noncomputable fintype instances. Second, these instances created diamonds with non-primed versions.

Estimated changes

Modified src/algebra/big_operators/basic.lean

modified theorem fintype.prod_subsingleton

Modified src/data/finite/basic.lean

deleted theorem of_subsingleton

Modified src/data/finset/basic.lean

added theorem finset.nonempty_iff_eq_singleton_default

Modified src/data/fintype/basic.lean

Modified src/ring_theory/noetherian.lean

Modified src/set_theory/cardinal/finite.lean