Commit 2026-06-21 18:23 617410ca

View on Github →

chore(Algebra/simp): remove @[simp] tag in AlgEquiv.coe_ringEquiv since it can be proven by simp (#40834) And deprecate AlgEquiv.coe_ringEquiv' as a duplicate of AlgEquiv.coe_ringEquiv.

Estimated changes

Modified Mathlib/Algebra/Algebra/Equiv.lean

deleted theorem AlgEquiv.coe_ringEquiv'

modified theorem AlgEquiv.coe_ringEquiv

Modified Mathlib/RingTheory/AdjoinRoot.lean

Modified scripts/nolints_prime_decls.txt