Commit 2023-06-14 02:21 af3b54c4

View on Github →

feat : port RingTheory.RingHom.Finite (#5013)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RingHom/Finite.lean

added theorem RingHom.finite_respectsIso

added theorem RingHom.finite_stableUnderBaseChange

added theorem RingHom.finite_stableUnderComposition