Commit 2024-07-24 12:52 e56a2050

View on Github →

refactor(RingTheory/Trace/Basic): remove Field assumptions (#15039) [Module.Free R S] [Module.Finite R S] replaces [FiniteDimensional K L]

Estimated changes

Modified Mathlib/RingTheory/Trace/Basic.lean

Modified Mathlib/RingTheory/Trace/Defs.lean

modified theorem Algebra.trace_algebraMap

modified theorem Algebra.trace_comp_trace

modified theorem Algebra.trace_trace