Commit 2025-12-07 22:48 a7af31ca

chore(RingTheory): generalize Algebra.intNorm (#32542) Generalize the definition of Algebra.intNorm by replacing Module.Finite A B by Algebra.IsIntegral A B and, in some cases, Algebra.IsAlgebraic (FractionRing A) (FractionRing B) or FiniteDimensional (FractionRing A) (FractionRing B). The goal being to eventually replace RingOfIntegers.norm by Algebra.intNorm Also delete many facts that can now be inferred directly