Commit 2023-06-26 04:12 37805e22

View on Github →

feat: port Algebra.Category.FGModule.basic (#4878) Sets new records for set_option maxHeartbeats. :-( I spent too long struggling with this one; if anyone would like to take another look please do.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Category/FGModuleCat/Basic.lean

added def FGModuleCat.FGModuleCatCoevaluation

added theorem FGModuleCat.FGModuleCatCoevaluation_apply_one

added def FGModuleCat.FGModuleCatDual

added theorem FGModuleCat.FGModuleCatDual_coe

added theorem FGModuleCat.FGModuleCatDual_obj

added def FGModuleCat.FGModuleCatEvaluation

added theorem FGModuleCat.FGModuleCatEvaluation_apply

added theorem FGModuleCat.Iso.conj_eq_conj

added def FGModuleCat.carrier

added def FGModuleCat.forget₂Monoidal

added theorem FGModuleCat.ihom_obj

added def FGModuleCat.isoToLinearEquiv

added def FGModuleCat.of

added theorem FGModuleCat.tensorObj_obj

added theorem FGModuleCat.tensorUnit_obj

added def FGModuleCat

added def LinearEquiv.toFGModuleCatIso

added theorem obj_carrier

Modified Mathlib/Algebra/Category/ModuleCat/Basic.lean

Modified Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean

Modified Mathlib/Algebra/Homology/ModuleCat.lean

Modified Mathlib/LinearAlgebra/Dual.lean

Modified Mathlib/RepresentationTheory/GroupCohomology/Resolution.lean