Commit 2023-06-16 04:31 4cf5b945

View on Github →

feat: port RingTheory.RingHom.FiniteType (#5075)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/RingHom/FiniteType.lean

added theorem RingHom.finiteType_holdsForLocalizationAway

added theorem RingHom.finiteType_is_local

added theorem RingHom.finiteType_ofLocalizationSpanTarget

added theorem RingHom.finiteType_respectsIso

added theorem RingHom.finiteType_stableUnderComposition