Theorem FreeAbelianGroup.of_injective

Modification history

2026-07-08 09:06
Mathlib/GroupTheory/FreeAbelianGroup.lean
chore: remove redundant `open scoped Classical` (#41423) …
Modified FreeAbelianGroup.of_injectiveView on Github →
2023-03-14 11:44
Mathlib/GroupTheory/FreeAbelianGroup.lean
feat: port GroupTheory.FreeAbelianGroup (#2247)
Added FreeAbelianGroup.of_injectiveView on Github →