Theorem Algebra.trace_prod_apply

Modification history

2024-07-09 09:58

Mathlib/RingTheory/Trace/Basic.lean

chore: Split `RingTheory.Trace` and `RingTheory.Norm` (#14446) …

Modified Algebra.trace_prod_apply View on Github →

2023-06-20 16:16

Mathlib/RingTheory/Trace.lean

feat: port RingTheory.Trace (#5256) …

Added Algebra.trace_prod_apply View on Github →