Commit 2023-05-20 14:27 3eaf5985

View on Github →

feat: port RingTheory.GradedAlgebra.Basic (#4143)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/GradedAlgebra/Basic.lean

added theorem DirectSum.coe_decompose_mul_add_of_left_mem

added theorem DirectSum.coe_decompose_mul_add_of_right_mem

added theorem DirectSum.coe_decompose_mul_of_left_mem

added theorem DirectSum.coe_decompose_mul_of_left_mem_of_le

added theorem DirectSum.coe_decompose_mul_of_left_mem_of_not_le

added theorem DirectSum.coe_decompose_mul_of_right_mem

added theorem DirectSum.coe_decompose_mul_of_right_mem_of_le

added theorem DirectSum.coe_decompose_mul_of_right_mem_of_not_le

added def DirectSum.decomposeAlgEquiv

added def DirectSum.decomposeRingEquiv

added theorem DirectSum.decompose_mul

added theorem DirectSum.decompose_mul_add_left

added theorem DirectSum.decompose_mul_add_right

added theorem DirectSum.decompose_one

added theorem DirectSum.decompose_symm_mul

added theorem DirectSum.decompose_symm_one

added theorem GradedAlgebra.mem_support_iff

added def GradedAlgebra.ofAlgHom

added def GradedAlgebra.proj

added theorem GradedAlgebra.proj_apply

added theorem GradedAlgebra.proj_recompose

added def GradedAlgebra

added theorem GradedRing.mem_support_iff

added def GradedRing.proj

added def GradedRing.projZeroRingHom

added theorem GradedRing.proj_apply

added theorem GradedRing.proj_recompose