mathlib

445154a5 - feat(group_theory/divisible): definition of divisible group (#15030)

feat(group_theory/divisible): definition of divisible group (#15030) This PR defines divisible group and proves that the set of rationals is divisible and product of divisible group is divisible. Future PR will be opened to prove that divisibility implies injectivity and hence category of abelian group has enough injective and an adjoint functor will transfer enough invectiveness in Ab to R-Mod.