mathlib
cadaa44a - feat(group_theory/subgroup): Add decidable_mem_range (#5371)

Commit

5 years ago

feat(group_theory/subgroup): Add decidable_mem_range (#5371) This means that `fintype (quotient_group.quotient f.range)` can be found by type-class resolution.

Author

eric-wieser

Parents

b2ab94f8

mathlib cadaa44a - feat(group_theory/subgroup): Add decidable_mem_range (#5371)

mathlib
cadaa44a - feat(group_theory/subgroup): Add decidable_mem_range (#5371)