Commit 2026-03-26 00:06 e7fcee2d
View on Github →feat(RingTheory): adds lemmas/instances related to integral maps to a field and residue fields (#36790) This PR adds some lemmas and instances related to integral maps to a field and residue fields.
feat(RingTheory): adds lemmas/instances related to integral maps to a field and residue fields (#36790) This PR adds some lemmas and instances related to integral maps to a field and residue fields.