Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-06-29 11:29 90d2046b

View on Github →

feat(algebra/monoid_algebra): adjointness for the functor G ↦ monoid_algebra k G when G carries only has_mul (#7932)

Estimated changes

Modified src/algebra/group_action_hom.lean

added theorem distrib_mul_action_hom.ext_ring

added theorem distrib_mul_action_hom.ext_ring_iff

added theorem distrib_mul_action_hom.to_add_monoid_hom_injective

added theorem distrib_mul_action_hom.to_mul_action_hom_injective

Modified src/algebra/module/linear_map.lean

added theorem distrib_mul_action_hom.coe_to_linear_map

added def distrib_mul_action_hom.to_linear_map

added theorem distrib_mul_action_hom.to_linear_map_eq_coe

added theorem distrib_mul_action_hom.to_linear_map_injective

Modified src/algebra/monoid_algebra.lean

added def add_monoid_algebra.lift_magma

added theorem add_monoid_algebra.non_unital_alg_hom_ext'

added theorem add_monoid_algebra.non_unital_alg_hom_ext

added def add_monoid_algebra.of_magma

added def monoid_algebra.lift_magma

added theorem monoid_algebra.non_unital_alg_hom_ext'

added theorem monoid_algebra.non_unital_alg_hom_ext

modified def monoid_algebra.of

deleted theorem monoid_algebra.of_apply

added def monoid_algebra.of_magma

Modified src/algebra/non_unital_alg_hom.lean

added theorem non_unital_alg_hom.to_distrib_mul_action_hom_injective

added theorem non_unital_alg_hom.to_mul_hom_injective

Modified src/data/finsupp/basic.lean

added def finsupp.distrib_mul_action_hom.single

added theorem finsupp.distrib_mul_action_hom_ext'

added theorem finsupp.distrib_mul_action_hom_ext