Theorem Algebra.coe_norm_int

Modification history

2023-11-20 10:21
Mathlib/NumberTheory/NumberField/Norm.lean
feat: add Algebra.coe_trace_int (#8513) …
Modified Algebra.coe_norm_intView on Github →
2023-11-19 10:31
Mathlib/NumberTheory/NumberField/Norm.lean
feat: move the lemma Algebra.coe_norm_int (#8481) …
Modified Algebra.coe_norm_intView on Github →
2023-10-03 10:19
Mathlib/NumberTheory/NumberField/Units.lean
feat: add Algebra.coe_norm_int (#7463) …
Added Algebra.coe_norm_intView on Github →