Rep

📁 Source: ClassFieldTheory/Mathlib/Algebra/Homology/ShortComplex/Rep.lean

Statistics

Metric	Count
Definitions instHasForget₂RepHomSubtypeModuleCatLinearMapIdCarrierVAbAddMonoidHomCarrier_classFieldTheory	1
Theorems rep_exact_iff_function_exact, rep_exact_iff, instAdditiveRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory, instPreservesColimitsRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory, instPreservesLimitsRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory	5
Total	6

CategoryTheory.ShortComplex

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rep_exact_iff 📖	—	—	—	—	instAdditiveRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory instPreservesLimitsRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory instPreservesColimitsRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory

CategoryTheory.ShortComplex.ShortExact

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
rep_exact_iff_function_exact 📖	—	—	—	—	—

(root)

Definitions

Name	Category	Theorems
instHasForget₂RepHomSubtypeModuleCatLinearMapIdCarrierVAbAddMonoidHomCarrier_classFieldTheory 📖	CompOp	3 math math: instPreservesColimitsRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory, instAdditiveRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory, instPreservesLimitsRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instAdditiveRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory 📖	mathematical	—	instHasForget₂RepHomSubtypeModuleCatLinearMapIdCarrierVAbAddMonoidHomCarrier_classFieldTheory	—	—
instPreservesColimitsRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory 📖	mathematical	—	instHasForget₂RepHomSubtypeModuleCatLinearMapIdCarrierVAbAddMonoidHomCarrier_classFieldTheory	—	—
instPreservesLimitsRepAbForget₂HomSubtypeModuleCatLinearMapIdCarrierVAddMonoidHomCarrier_classFieldTheory 📖	mathematical	—	instHasForget₂RepHomSubtypeModuleCatLinearMapIdCarrierVAbAddMonoidHomCarrier_classFieldTheory	—	—

---

← Back to Index