Theorem AddSubmonoid.toNatSubmodule_closure

Modification history

2025-06-14 13:55
Mathlib/LinearAlgebra/Span/Basic.lean
feat(NumberTheory): discriminant is norm of different (#25792)
Added AddSubmonoid.toNatSubmodule_closureView on Github →