Commit 2023-11-29 14:38 c5035213

View on Github →

feat(RepresentationTheory/GroupCohomology): Noether's generalization of Hilbert's Theorem 90 (#8599)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Algebra/Equiv.lean

Modified Mathlib/Algebra/Algebra/Hom.lean

Modified Mathlib/Algebra/Group/Equiv/TypeTags.lean

added def addMonoidEndToMultiplicative

added def monoidEndToAdditive

Modified Mathlib/LinearAlgebra/Basic.lean

added def addMonoidEndRingEquivInt

Modified Mathlib/RepresentationTheory/Basic.lean

added def Representation.ofDistribMulAction

added theorem Representation.ofDistribMulAction_apply_apply

added def Representation.ofMulDistribMulAction

added theorem Representation.ofMulDistribMulAction_apply_apply

Created Mathlib/RepresentationTheory/GroupCohomology/Hilbert90.lean

added theorem Hilbert90.aux_ne_zero

added theorem hilbert90

Modified Mathlib/RepresentationTheory/Rep.lean

added def Rep.ofAlgebraAut

added def Rep.ofAlgebraAutOnUnits

added def Rep.ofDistribMulAction

added theorem Rep.ofDistribMulAction_ρ_apply_apply

added def Rep.ofMulDistribMulAction

added theorem Rep.ofMulDistribMulAction_ρ_apply_apply