Commit 2026-05-11 14:41 5842b73d

View on Github →

feat: add more API for (rel)index and ideals (#39118) This adds a few more API lemmas for {Add|}Subgroup.{FiniteIndex|IsFiniteRelIndex} and connects the index with Ideal.absNorm; we also add the fact that (relative) indices of nonzero ideals in a Dedekind domain that is finite and free over the integers are finite. We also generalize Algebra.norm_algebraMap from base fields to commutative rings, assuming the algebra is free over the base ring, and add some more API (Algebra.del_lsmul, Algebra.norm_natCast).

Estimated changes

Modified Mathlib/Algebra/Algebra/Tower.lean

added theorem Algebra.lsmul_apply

added theorem Algebra.lsmul_eq_smul_one

Modified Mathlib/GroupTheory/FiniteAbelian/Basic.lean

Modified Mathlib/GroupTheory/Index.lean

added theorem Subgroup.isFiniteRelIndex_of_finiteIndex

deleted theorem Subgroup.isFiniteRelIndex_of_le

added theorem Subgroup.isFiniteRelIndex_of_le_left

added theorem Subgroup.isFiniteRelIndex_of_le_right

added theorem Subgroup.isFiniteRelIndex_top_iff

Modified Mathlib/LinearAlgebra/Determinant.lean

added theorem Algebra.det_lsmul

Modified Mathlib/RingTheory/Ideal/Norm/AbsNorm.lean

added theorem Ideal.absNorm_eq_index

added theorem Ideal.absNorm_span_natCast

added theorem Ideal.finiteIndex

added theorem Ideal.isFiniteRelIndex

Modified Mathlib/RingTheory/Ideal/Operations.lean

added theorem Ideal.inf_ne_bot_of_ne_bot

Modified Mathlib/RingTheory/Norm/Defs.lean