Theorem AddSubgroup.toIntSubmodule_closure

Modification history

2025-06-14 13:55

Mathlib/LinearAlgebra/Span/Basic.lean

feat(NumberTheory): discriminant is norm of different (#25792)

Added AddSubgroup.toIntSubmodule_closure View on Github →