Commit 2023-05-16 15:19 ecb752ad

View on Github →

chore: cleanup various notes about etaExperiment (#4029)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Finsupp.lean

modified def finsuppLEquivDirectSum

Modified Mathlib/RingTheory/Finiteness.lean

Modified Mathlib/RingTheory/Ideal/Prod.lean

Modified Mathlib/RingTheory/QuotientNilpotent.lean

Modified Mathlib/Topology/Algebra/Ring/Ideal.lean