Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-12-13 03:30 c55911f6

View on Github →

chore(order/atoms): split out finiteness results (#17866)

Estimated changes

Modified src/group_theory/subgroup/basic.lean

Modified src/group_theory/sylow.lean

Modified src/order/atoms.lean

deleted theorem fintype.is_simple_order.card

deleted theorem fintype.is_simple_order.univ

Created src/order/atoms/finite.lean

added theorem fintype.is_simple_order.card

added theorem fintype.is_simple_order.univ

Modified src/order/partition/finpartition.lean