Def class_group
Modification history
2022-10-08 20:02
src/ring_theory/class_group.lean
refactor(ring_theory/class_group): redefine class_group without fraction field (#16727) …
Modified class_groupView on Github →2022-01-05 23:45
src/ring_theory/class_group.lean
chore(*): notation for `units` (#11236)
Modified class_groupView on Github →