Theorem ClassGroup.exists_mem_finset_approx'

Modification history

2024-05-16 14:20

Mathlib/NumberTheory/ClassNumber/Finite.lean

refactor: Turn Algebra.IsAlgebraic and Algebra.IsIntegral into classes (#12761) …

Modified ClassGroup.exists_mem_finset_approx'View on Github →

2023-06-24 15:15

Mathlib/NumberTheory/ClassNumber/Finite.lean

feat: port NumberTheory.ClassNumber.Finite (#5337)

Added ClassGroup.exists_mem_finset_approx'View on Github →