Theorem NumberField.inverse_basisMatrix_mulVec_eq_repr

Modification history

2024-08-08 10:31
Mathlib/NumberTheory/NumberField/EquivReindex.lean
chore: backports for leanprover/lean4#4814 (part 36) (#15612)
Modified NumberField.inverse_basisMatrix_mulVec_eq_reprView on Github →
2024-07-23 13:52
Mathlib/NumberTheory/NumberField/EquivReindex.lean
feat: the `House` of an algebraic number (#14041) …
Added NumberField.inverse_basisMatrix_mulVec_eq_reprView on Github →