Def RatFunc.coeAlgHom

Modification history

2024-10-10 07:46

Mathlib/RingTheory/LaurentSeries.lean

feat(RingTheory/LaurentSeries): add notation (#16639) …

Modified RatFunc.coeAlgHom View on Github →

2024-05-20 10:05

Mathlib/FieldTheory/RatFunc/Basic.lean

chore(FieldTheory/RatFunc): split the file into several ones (#12425) …

Modified RatFunc.coeAlgHom View on Github →

2023-05-25 21:39

Mathlib/FieldTheory/RatFunc.lean

feat: port FieldTheory.Ratfunc (#4293) …

Added RatFunc.coeAlgHom View on Github →