Documentation

Mathlib.Algebra.Group.TypeTags.Finite

Finite and Infinite are preserved by Additive and Multiplicative. #

instance instFiniteAdditive {α : Type u} [Finite α] :
instance instInfiniteAdditive {α : Type u} [h : Infinite α] :