Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-07-11 22:33 52d4daef

View on Github →

feat(representation_theory/monoid_algebra_basis): add some API for k[G^n] (#14308)

Estimated changes

Modified src/algebra/big_operators/fin.lean

added def fin.partial_prod

added theorem fin.partial_prod_succ'

added theorem fin.partial_prod_succ

added theorem fin.partial_prod_zero

modified theorem list.prod_of_fn

modified theorem list.prod_take_of_fn

Modified src/representation_theory/basic.lean

added theorem representation.of_mul_action_apply

added theorem representation.of_mul_action_def

Created src/representation_theory/group_cohomology_resolution.lean

added def Rep.of_mul_action

added def group_cohomology.resolution.of_tensor

added def group_cohomology.resolution.of_tensor_aux

added theorem group_cohomology.resolution.of_tensor_aux_comm_of_mul_action

added theorem group_cohomology.resolution.of_tensor_aux_single

added theorem group_cohomology.resolution.of_tensor_single'

added theorem group_cohomology.resolution.of_tensor_single

added def group_cohomology.resolution.to_tensor

added def group_cohomology.resolution.to_tensor_aux

added theorem group_cohomology.resolution.to_tensor_aux_of_mul_action

added theorem group_cohomology.resolution.to_tensor_aux_single

added theorem group_cohomology.resolution.to_tensor_single