Commit 2021-01-27 18:19 8af7e08e

View on Github →

feat(data/fintype/basic): make subtype_of_fintype computable (#5919) This smokes out a few places downstream that are missing decidability hypotheses needed for the fintype instance to exist.

Estimated changes

Modified src/combinatorics/simple_graph/basic.lean

Modified src/combinatorics/simple_graph/degree_sum.lean

modified theorem simple_graph.even_card_odd_degree_vertices

modified theorem simple_graph.exists_ne_odd_degree_of_exists_odd_degree

modified theorem simple_graph.odd_card_odd_degree_vertices_ne

Modified src/data/fintype/basic.lean

Modified src/data/fintype/card.lean

Modified src/field_theory/galois.lean

Modified src/group_theory/order_of_element.lean

Modified src/group_theory/perm/subgroup.lean

Modified src/group_theory/subgroup.lean

modified theorem subgroup.eq_top_of_card_eq