Commit 2025-02-18 10:05 a1fd9f15

View on Github →

chore(Algebra/Ring/Subring): avoid importing Int.Cast.Lemmas in Defs.lean (#21997) The file Data.Int.Cast.Lemmas is quite theory-heavy in itself, and brings along a lot more. We can get rid of the import by replacing a couple proofs with rfl and moving a lemma to a downstream file.

Estimated changes

Modified Mathlib/Algebra/Ring/Subring/Basic.lean

added theorem AddSubgroup.int_mul_mem

Modified Mathlib/Algebra/Ring/Subring/Defs.lean

deleted theorem AddSubgroup.int_mul_mem

modified theorem Subring.coe_intCast

modified theorem Subring.coe_natCast

modified theorem SubringClass.coe_intCast

modified theorem SubringClass.coe_natCast