Def Algebra.Extension.Hom.mapKer

Modification history

2025-01-20 11:48

Mathlib/RingTheory/Extension.lean

feat(RingTheory): `H¹(L)` under localization (#20591)

Added Algebra.Extension.Hom.mapKer View on Github →