Mathlib v3 is deprecated. Go to Mathlib v4

Def associated

Modification history

2022-01-05 23:45

src/algebra/associated.lean

chore(*): notation for `units` (#11236)

Modified associated View on Github →

2018-09-02 20:50

ring_theory/associated_elements.lean

feat(ring_theory): add associated elements

Added associated View on Github →