mathlib

725ad273 - feat(algebra/direct_sum/decomposition): add an induction principle for `direct_sum.decomposition` class (#15654)

feat(algebra/direct_sum/decomposition): add an induction principle for `direct_sum.decomposition` class (#15654) If `direct_sum.decomposition M` and `p : M → Prop`, then to prove `p m` for an arbitrary `m`, it suffices to prove `p 0` and `p x` for homogeneous x and `p` being preserved by add.