Commit 2023-11-20 10:21 72756259

View on Github →

feat: add Algebra.coe_trace_int (#8513) From flt-regular.

Estimated changes

modified theorem Algebra.coe_norm_int
added theorem Algebra.coe_trace_int