Commit 2023-01-30 11:13 d16fa2fb

View on Github →

feat: port Algebra.DirectSum.Basic (#1923) Needed to add some instance names in Dfinnsup/Basic because the standard ones were insanely long. Could extract that to a separate PR, but maybe that's not needed.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/DirectSum/Basic.lean

added theorem DirectSum.IsInternal.addSubmonoid_supᵢ_eq_top

added def DirectSum.IsInternal

added theorem DirectSum.addHom_ext'

added theorem DirectSum.addHom_ext

added theorem DirectSum.add_apply

added theorem DirectSum.coeAddMonoidHom_of

added theorem DirectSum.coe_of_apply

added def DirectSum.equivCongrLeft

added theorem DirectSum.equivCongrLeft_apply

added def DirectSum.fromAddMonoid

added theorem DirectSum.fromAddMonoid_of

added theorem DirectSum.fromAddMonoid_of_apply

added def DirectSum.mk

added theorem DirectSum.mk_injective

added def DirectSum.of

added theorem DirectSum.of_eq_of_ne

added theorem DirectSum.of_eq_same

added theorem DirectSum.of_injective

added def DirectSum.setToSet

added theorem DirectSum.sigmaCurry_apply

added theorem DirectSum.sigmaUncurry_apply

added theorem DirectSum.sub_apply

added theorem DirectSum.sum_support_of

added theorem DirectSum.support_of

added theorem DirectSum.support_of_subset

added theorem DirectSum.support_zero

added theorem DirectSum.toAddMonoid.unique

added def DirectSum.toAddMonoid

added theorem DirectSum.toAddMonoid_of

added theorem DirectSum.zero_apply

added def DirectSum