Commit 2021-12-05 16:33 8c1f2b5d

View on Github →

feat(ring_theory/graded_algebra): projection map of graded algebra (#10116) This pr defines and proves some property about graded_algebra.proj : A →ₗ[R] A

Estimated changes

Modified src/algebra/direct_sum/basic.lean

added theorem direct_sum.coe_of_add_subgroup_apply

added theorem direct_sum.coe_of_add_submonoid_apply

Modified src/algebra/direct_sum/internal.lean

added theorem direct_sum.coe_mul_apply_add_subgroup

added theorem direct_sum.coe_mul_apply_add_submonoid

added theorem direct_sum.coe_mul_apply_submodule

Modified src/algebra/direct_sum/module.lean

added theorem direct_sum.coe_of_submodule_apply

Modified src/algebra/direct_sum/ring.lean

added theorem direct_sum.mul_eq_sum_support_ghas_mul

Modified src/group_theory/subgroup/basic.lean

added theorem subgroup.coe_finset_prod

added theorem subgroup.coe_list_prod

added theorem subgroup.coe_multiset_prod

Modified src/ring_theory/graded_algebra/basic.lean

added theorem graded_algebra.decompose_coe

added theorem graded_algebra.decompose_of_mem

added theorem graded_algebra.decompose_of_mem_ne

added theorem graded_algebra.decompose_of_mem_same

added theorem graded_algebra.is_internal

added theorem graded_algebra.mem_support_iff

added def graded_algebra.proj

added theorem graded_algebra.proj_apply

added theorem graded_algebra.proj_recompose

added theorem graded_algebra.sum_support_decompose

added def graded_algebra.support

deleted theorem graded_ring.is_internal