Commit 2026-10-19 10:12 f3e8c297

View on Github →

feat(RingTheory/Unramified/Finite): elem is idempotent (#44966) This PR proves that Algebra.FormallyUnramified.elem is always idempotent.

Estimated changes

Modified Mathlib/RingTheory/Unramified/Finite.lean

added theorem Algebra.FormallyUnramified.isIdempotentElem_elem

modified theorem Algebra.FormallyUnramified.lmul_elem

modified theorem Algebra.FormallyUnramified.one_tmul_mul_elem

modified theorem Algebra.FormallyUnramified.one_tmul_sub_tmul_one_mul_elem