Theorem RingHom.FiniteType.id

Modification history

2025-08-13 10:56

Mathlib/RingTheory/FiniteType.lean

refactor: use `Algebra.FiniteType` as a class (#27030) …

Modified RingHom.FiniteType.id View on Github →

2023-04-03 20:29

Mathlib/RingTheory/FiniteType.lean

feat: port RingTheory.FiniteType (#3241)

Added RingHom.FiniteType.id View on Github →