Commit 2025-01-10 00:02 66b1e307

View on Github →

chore: ext lemma for DirectSum (#20600)

Estimated changes

Modified Mathlib/Algebra/DirectSum/Basic.lean

added theorem DirectSum.ext

Modified Mathlib/Algebra/DirectSum/Module.lean

deleted theorem DirectSum.ext

added theorem DirectSum.ext_component

added theorem DirectSum.ext_component_iff

deleted theorem DirectSum.ext_iff

Modified Mathlib/Algebra/DirectSum/Ring.lean

Modified Mathlib/Algebra/Lie/DirectSum.lean

Modified Mathlib/RingTheory/AdicCompletion/Functoriality.lean

Modified Mathlib/RingTheory/Flat/Basic.lean