Def local_ring.residue_field
Modification history
2021-12-04 01:52
src/ring_theory/ideal/local_ring.lean
feat(*): `A ⧸ B` notation for quotients in algebra (#10501) …
Modified local_ring.residue_fieldView on Github →2021-08-25 06:39
src/ring_theory/ideal/basic.lean
chore(ring_theory/ideal): Move local rings into separate file (#8849) …
Modified local_ring.residue_fieldView on Github →