Commit 2025-01-21 01:06 ba4ffc06

View on Github →

refactor(LinearAlgebra/Projection): Use IsIdempotentElem (#20665) Use IsIdempotentElem in a number of locations instead of ? * ? = ?.

  • Algebra/Algebra/Subalgebra/Pointwise
  • Algebra/Ring/BooleanRing
  • LinearAlgebra/Projection
  • RingTheory/DedekindDomain/Ideal Other uses of ? * ? = ? are not rings or have to_additive, which our current definition of IsIdempotentElem does not support. My interest in opening this PR is LinearAlgebra/Projection. The others are perhaps more tenuous. I have made them individual commits so any not required can easily be reverted.

Estimated changes

deleted theorem Subalgebra.mul_self
added theorem BooleanRing.mul_self