Namespace `ClassGroup` 1 theorems

A finite set of primes supporting all ideal classes ClassGroup.exists_finset_forall_exists_mk0_eq_of_dvd 0 below · cited by 3 · depth 13

Documents the Lean sources in this repository (Lean v4.33.1, Mathlib v4.33.0). Statements are quoted textually from the .lean files; dependency edges are the import Theorems.Thm_… lines of the proof modules. About these pages.

Namespace ClassGroup 1 theorems

Namespace `ClassGroup` 1 theorems