Theorem NumberField.mem_span_integralBasis

Modification history

2023-08-02 09:22

Mathlib/NumberTheory/NumberField/Basic.lean

feat(NumberTheory.NumberField.Basic): add mem_span_integralBasis (#5996) …

Added NumberField.mem_span_integralBasis View on Github →