Loogle!
Result
Found 97 definitions mentioning Units, Int, Int.instMonoid and HSMul.hSMul. Of these, 97 match your pattern(s).
- ZMod.smul_units_def Mathlib.Data.ZMod.IntUnitsPower
∀ (z : ZMod 2) (au : Additive ℤˣ), z • au = z.val • au - ZMod.natCast_smul_units Mathlib.Data.ZMod.IntUnitsPower
∀ (n : ℕ) (au : Additive ℤˣ), ↑n • au = n • au - ofMul_uzpow Mathlib.Data.ZMod.IntUnitsPower
∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (u : ℤˣ) (r : R), Additive.ofMul (u ^ r) = r • Additive.ofMul u - toMul_uzpow Mathlib.Data.ZMod.IntUnitsPower
∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : Module R (Additive ℤˣ)] (u : Additive ℤˣ) (r : R), Additive.toMul (r • u) = Additive.toMul u ^ r - AlternatingMap.map_congr_perm Mathlib.LinearAlgebra.Alternating.Basic
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6} [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') (v : ι → M) [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (σ : Equiv.Perm ι), g v = Equiv.Perm.sign σ • g (v ∘ ⇑σ) - AlternatingMap.map_perm Mathlib.LinearAlgebra.Alternating.Basic
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6} [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [inst_5 : DecidableEq ι] [inst_6 : Fintype ι] (v : ι → M) (σ : Equiv.Perm ι), g (v ∘ ⇑σ) = Equiv.Perm.sign σ • g v - AlternatingMap.domDomCongr_perm Mathlib.LinearAlgebra.Alternating.Basic
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6} [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} (g : M [⋀^ι]→ₗ[R] N') [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (σ : Equiv.Perm ι), AlternatingMap.domDomCongr σ g = Equiv.Perm.sign σ • g - MultilinearMap.alternatization_apply Mathlib.LinearAlgebra.Alternating.Basic
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6} [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (m : MultilinearMap R (fun x => M) N') (v : ι → M), (MultilinearMap.alternatization m) v = Finset.univ.sum fun σ => Equiv.Perm.sign σ • (MultilinearMap.domDomCongr σ m) v - MultilinearMap.alternatization_coe Mathlib.LinearAlgebra.Alternating.Basic
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6} [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (m : MultilinearMap R (fun x => M) N'), ↑(MultilinearMap.alternatization m) = Finset.univ.sum fun σ => Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m - MultilinearMap.alternatization_def Mathlib.LinearAlgebra.Alternating.Basic
∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N' : Type u_6} [inst_3 : AddCommGroup N'] [inst_4 : Module R N'] {ι : Type u_7} [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] (m : MultilinearMap R (fun x => M) N'), ⇑(MultilinearMap.alternatization m) = ⇑(Finset.univ.sum fun σ => Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ m) - Matrix.det_neg_eq_smul Mathlib.LinearAlgebra.Matrix.Determinant
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (A : Matrix n n R), (-A).det = (-1) ^ Fintype.card n • A.det - Matrix.det_apply Mathlib.LinearAlgebra.Matrix.Determinant
∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R), M.det = Finset.univ.sum fun σ => Equiv.Perm.sign σ • Finset.univ.prod fun i => M (σ i) i - CategoryTheory.Preadditive.smul_iso_hom Mathlib.CategoryTheory.Preadditive.Basic
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (a : ℤˣ) (e : X ≅ Y), (a • e).hom = a • e.hom - CategoryTheory.Preadditive.smul_iso_inv Mathlib.CategoryTheory.Preadditive.Basic
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (a : ℤˣ) (e : X ≅ Y), (a • e).inv = a⁻¹ • e.inv - CategoryTheory.NatTrans.app_units_zsmul Mathlib.CategoryTheory.Preadditive.FunctorCategory
∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Category.{u_3, u_2} D] [inst_2 : CategoryTheory.Preadditive D] {F G : CategoryTheory.Functor C D} (X : C) (α : F ⟶ G) (n : ℤˣ), (n • α).app X = n • α.app X - HomologicalComplex₂.d₂_eq' Mathlib.Algebra.Homology.TotalComplex
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [inst_2 : DecidableEq I₁₂] [inst_3 : TotalComplexShape c₁ c₂ c₁₂] [inst_4 : K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → ∀ (i₁₂ : I₁₂), K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotalOrZero c₁₂ i₁ i₂' i₁₂) - HomologicalComplex₂.d₂_eq Mathlib.Algebra.Homology.TotalComplex
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [inst_2 : DecidableEq I₁₂] [inst_3 : TotalComplexShape c₁ c₂ c₁₂] [inst_4 : K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → ∀ (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂), K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.ιTotal c₁₂ i₁ i₂' i₁₂ h') - HomologicalComplex₂.d₁_eq' Mathlib.Algebra.Homology.TotalComplex
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [inst_2 : DecidableEq I₁₂] [inst_3 : TotalComplexShape c₁ c₂ c₁₂] [inst_4 : K.HasTotal c₁₂] {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂) (i₁₂ : I₁₂), K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotalOrZero c₁₂ i₁' i₂ i₁₂) - HomologicalComplex₂.totalAux.d₂_eq' Mathlib.Algebra.Homology.TotalComplex
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [inst_2 : DecidableEq I₁₂] [inst_3 : TotalComplexShape c₁ c₂ c₁₂] [inst_4 : K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → ∀ (i₁₂ : I₁₂), K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂) - HomologicalComplex₂.totalAux.d₂_eq Mathlib.Algebra.Homology.TotalComplex
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [inst_2 : DecidableEq I₁₂] [inst_3 : TotalComplexShape c₁ c₂ c₁₂] [inst_4 : K.HasTotal c₁₂] (i₁ : I₁) {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → ∀ (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁, i₂') = i₁₂), K.d₂ c₁₂ i₁ i₂ i₁₂ = c₁.ε₂ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.X i₁).d i₂ i₂') (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁, i₂') i₁₂ h') - HomologicalComplex₂.d₁_eq Mathlib.Algebra.Homology.TotalComplex
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [inst_2 : DecidableEq I₁₂] [inst_3 : TotalComplexShape c₁ c₂ c₁₂] [inst_4 : K.HasTotal c₁₂] {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂), K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.ιTotal c₁₂ i₁' i₂ i₁₂ h') - HomologicalComplex₂.totalAux.d₁_eq' Mathlib.Algebra.Homology.TotalComplex
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [inst_2 : DecidableEq I₁₂] [inst_3 : TotalComplexShape c₁ c₂ c₁₂] [inst_4 : K.HasTotal c₁₂] {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂) (i₁₂ : I₁₂), K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.toGradedObject.ιMapObjOrZero (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂) - HomologicalComplex₂.totalAux.d₁_eq Mathlib.Algebra.Homology.TotalComplex
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2} {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c₁₂ : ComplexShape I₁₂) [inst_2 : DecidableEq I₁₂] [inst_3 : TotalComplexShape c₁ c₂ c₁₂] [inst_4 : K.HasTotal c₁₂] {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ (i₂ : I₂) (i₁₂ : I₁₂) (h' : c₁.π c₂ c₁₂ (i₁', i₂) = i₁₂), K.d₁ c₁₂ i₁ i₂ i₁₂ = c₁.ε₁ c₂ c₁₂ (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((K.d i₁ i₁').f i₂) (K.toGradedObject.ιMapObj (c₁.π c₂ c₁₂) (i₁', i₂) i₁₂ h') - HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁ Mathlib.Algebra.Homology.BifunctorHomotopy
∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [inst : CategoryTheory.Category.{u_9, u_1} C₁] [inst_1 : CategoryTheory.Category.{u_8, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_7, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J] [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c] (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : c₁.π c₂ c (i₁', i₂) = j), c₁.prev i₁' = i₁ → CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h) (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j') = c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j')) - HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₁_assoc Mathlib.Algebra.Homology.BifunctorHomotopy
∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [inst : CategoryTheory.Category.{u_9, u_1} C₁] [inst_1 : CategoryTheory.Category.{u_8, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_7, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J] [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c] (i₁ i₁' : I₁) (i₂ : I₂) (j j' : J) (h : c₁.π c₂ c (i₁', i₂) = j), c₁.prev i₁' = i₁ → ∀ {Z : D} (h_1 : (L₁.mapBifunctor L₂ F c).X j' ⟶ Z), CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁' i₂ j h) (CategoryTheory.CategoryStruct.comp (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c j j') h_1) = CategoryTheory.CategoryStruct.comp (c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))) h_1 - HomologicalComplex.mapBifunctorMapHomotopy.comm₁_aux Mathlib.Algebra.Homology.BifunctorHomotopy
∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6} [inst : CategoryTheory.Category.{u_9, u_1} C₁] [inst_1 : CategoryTheory.Category.{u_8, u_2} C₂] [inst_2 : CategoryTheory.Category.{u_7, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} {f₁ f₁' : K₁ ⟶ L₁} (h₁ : Homotopy f₁ f₁') {K₂ L₂ : HomologicalComplex C₂ c₂} (f₂ : K₂ ⟶ L₂) (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J] [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c] {i₁ i₁' : I₁}, c₁.Rel i₁ i₁' → ∀ {i₂ i₂' : I₂}, c₂.Rel i₂ i₂' → ∀ (j : J), c₁.π c₂ c (i₁', i₂) = j → c₁.ε₁ c₂ c (i₁, i₂) • CategoryTheory.CategoryStruct.comp ((F.map (h₁.hom i₁' i₁)).app (K₂.X i₂)) (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (f₂.f i₂)) ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj L₁).obj L₂).d₂ c i₁ i₂ j)) = -CategoryTheory.CategoryStruct.comp ((((F.mapBifunctorHomologicalComplex c₁ c₂).obj K₁).obj K₂).d₂ c i₁' i₂ (c.next j)) (HomologicalComplex.mapBifunctorMapHomotopy.hom₁ h₁ f₂ F c (c.next j) j) - CochainComplex.shiftFunctor_obj_d Mathlib.Algebra.Homology.HomotopyCategory.Shift
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ) (K : CochainComplex C ℤ) (i j : ℤ), ((CochainComplex.shiftFunctor C n).obj K).d i j = n.negOnePow • K.d (i + n) (j + n) - CochainComplex.shiftFunctor_obj_d' Mathlib.Algebra.Homology.HomotopyCategory.Shift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (K : CochainComplex C ℤ) (n i j : ℤ), ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j = n.negOnePow • K.d (i + { as := n }.as) (j + { as := n }.as) - CochainComplex.shiftFunctor_map_f Mathlib.Algebra.Homology.HomotopyCategory.Shift
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] (n : ℤ) {X Y : CochainComplex C ℤ} (φ : X ⟶ Y) (i : ℤ), ((CochainComplex.shiftFunctor C n).map φ).f i = φ.f (i + n) - HomologicalComplex₂.D₁_totalShift₁XIso_hom Mathlib.Algebra.Homology.TotalComplexShift
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁'), CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁') - HomologicalComplex₂.D₁_totalShift₂XIso_hom Mathlib.Algebra.Homology.TotalComplexShift
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁'), CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁') - HomologicalComplex₂.D₂_totalShift₁XIso_hom Mathlib.Algebra.Homology.TotalComplexShift
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁'), CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₁XIso x n₁ n₁' h₁).hom = x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁') - HomologicalComplex₂.D₂_totalShift₂XIso_hom Mathlib.Algebra.Homology.TotalComplexShift
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁'), CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (K.totalShift₂XIso y n₁ n₁' h₁).hom = y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁') - HomologicalComplex₂.D₁_totalShift₁XIso_hom_assoc Mathlib.Algebra.Homology.TotalComplexShift
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z), CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')) h - HomologicalComplex₂.D₁_totalShift₂XIso_hom_assoc Mathlib.Algebra.Homology.TotalComplexShift
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z), CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₁ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₁ (ComplexShape.up ℤ) n₀' n₁')) h - HomologicalComplex₂.D₂_totalShift₁XIso_hom_assoc Mathlib.Algebra.Homology.TotalComplexShift
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : ((HomologicalComplex₂.shiftFunctor₁ C x).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + x = n₀') (h₁ : n₁ + x = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z), CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (x.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₁XIso x n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')) h - HomologicalComplex₂.D₂_totalShift₂XIso_hom_assoc Mathlib.Algebra.Homology.TotalComplexShift
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (y : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)] [inst_3 : ((HomologicalComplex₂.shiftFunctor₂ C y).obj K).HasTotal (ComplexShape.up ℤ)] (n₀ n₁ n₀' n₁' : ℤ) (h₀ : n₀ + y = n₀') (h₁ : n₁ + y = n₁') {Z : C} (h : (K.total (ComplexShape.up ℤ)).X n₁' ⟶ Z), CategoryTheory.CategoryStruct.comp (((HomologicalComplex₂.shiftFunctor₂ C y).obj K).D₂ (ComplexShape.up ℤ) n₀ n₁) (CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₁ n₁' h₁).hom h) = CategoryTheory.CategoryStruct.comp (y.negOnePow • CategoryTheory.CategoryStruct.comp (K.totalShift₂XIso y n₀ n₀' h₀).hom (K.D₂ (ComplexShape.up ℤ) n₀' n₁')) h - CochainComplex.HomComplex.δ_zero_cochain_comp Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G 0) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (m₂ : ℤ) (h₂ : n₂ + 1 = m₂), CochainComplex.HomComplex.δ n₂ m₂ (z₁.comp z₂ ⋯) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ 0 1 z₁).comp z₂ ⋯ - CochainComplex.HomComplex.δ_comp Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {F G K : CochainComplex C ℤ} {n₁ n₂ n₁₂ : ℤ} (z₁ : CochainComplex.HomComplex.Cochain F G n₁) (z₂ : CochainComplex.HomComplex.Cochain G K n₂) (h : n₁ + n₂ = n₁₂) (m₁ m₂ m₁₂ : ℤ) (h₁₂ : n₁₂ + 1 = m₁₂) (h₁ : n₁ + 1 = m₁) (h₂ : n₂ + 1 = m₂), CochainComplex.HomComplex.δ n₁₂ m₁₂ (z₁.comp z₂ h) = z₁.comp (CochainComplex.HomComplex.δ n₂ m₂ z₂) ⋯ + n₂.negOnePow • (CochainComplex.HomComplex.δ n₁ m₁ z₁).comp z₂ ⋯ - CochainComplex.HomComplex.δ_v Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (n m : ℤ) (hnm : n + 1 = m) (z : CochainComplex.HomComplex.Cochain F G n) (p q : ℤ) (hpq : p + m = q) (q₁ q₂ : ℤ) (hq₁ : q₁ = q - 1) (hq₂ : p + 1 = q₂), (CochainComplex.HomComplex.δ n m z).v p q hpq = CategoryTheory.CategoryStruct.comp (z.v p q₁ ⋯) (G.d q₁ q) + m.negOnePow • CategoryTheory.CategoryStruct.comp (F.d p q₂) (z.v q₂ q ⋯) - CochainComplex.mappingCone.descCocycle Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
{C : Type u_1} → [inst : CategoryTheory.Category.{u_2, u_1} C] → [inst_1 : CategoryTheory.Preadditive C] → {F G : CochainComplex C ℤ} → (φ : F ⟶ G) → [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] → {K : CochainComplex C ℤ} → {n m : ℤ} → (α : CochainComplex.HomComplex.Cochain F K m) → (β : CochainComplex.HomComplex.Cocycle G K n) → m + 1 = n → CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯ → CochainComplex.HomComplex.Cocycle (CochainComplex.mappingCone φ) K n - CochainComplex.mappingCone.descCocycle_coe Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cocycle G K n) (h : m + 1 = n) (eq : CochainComplex.HomComplex.δ m n α = n.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp ↑β ⋯), ↑(CochainComplex.mappingCone.descCocycle φ α β h eq) = CochainComplex.mappingCone.descCochain φ α (↑β) h - CochainComplex.mappingCone.δ_descCochain Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ} {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n) (n' : ℤ) (hn' : n + 1 = n'), CochainComplex.HomComplex.δ n n' (CochainComplex.mappingCone.descCochain φ α β h) = (↑(CochainComplex.mappingCone.fst φ)).comp (CochainComplex.HomComplex.δ m n α + n'.negOnePow • (CochainComplex.HomComplex.Cochain.ofHom φ).comp β ⋯) ⋯ + (CochainComplex.mappingCone.snd φ).comp (CochainComplex.HomComplex.δ n n' β) ⋯ - CochainComplex.HomComplex.Cochain.δ_leftUnshift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {a n' : ℤ} (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (m m' : ℤ) (hm' : m + a = m'), CochainComplex.HomComplex.δ n m (γ.leftUnshift n hn) = a.negOnePow • (CochainComplex.HomComplex.δ n' m' γ).leftUnshift m hm' - CochainComplex.HomComplex.Cochain.δ_rightUnshift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {a n' : ℤ} (γ : CochainComplex.HomComplex.Cochain K ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj L) n') (n : ℤ) (hn : n' + a = n) (m m' : ℤ) (hm' : m' + a = m), CochainComplex.HomComplex.δ n m (γ.rightUnshift n hn) = a.negOnePow • (CochainComplex.HomComplex.δ n' m' γ).rightUnshift m hm' - CochainComplex.HomComplex.Cochain.δ_leftShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' m' : ℤ) (hn' : n + a = n') (m : ℤ) (hm' : m + a = m'), CochainComplex.HomComplex.δ n' m' (γ.leftShift a n' hn') = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).leftShift a m' hm' - CochainComplex.HomComplex.Cochain.δ_rightShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' m' : ℤ) (hn' : n' + a = n) (m : ℤ) (hm' : m' + a = m), CochainComplex.HomComplex.δ n' m' (γ.rightShift a n' hn') = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).rightShift a m' hm' - CochainComplex.HomComplex.Cochain.leftShift_comp Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L M : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n') {m t t' : ℤ} (γ' : CochainComplex.HomComplex.Cochain L M m) (h : n + m = t) (ht' : t + a = t'), (γ.comp γ' h).leftShift a t' ht' = (a * m).negOnePow • (γ.leftShift a n' hn').comp γ' ⋯ - CochainComplex.HomComplex.Cochain.leftShift_v Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n') (p q : ℤ) (hpq : p + n' = q) (p' : ℤ) (hp' : p' + n = q), (γ.leftShift a n' hn').v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p p' ⋯).hom (γ.v p' q hp') - CochainComplex.HomComplex.Cochain.leftShift_rightShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n' + a = n), (γ.rightShift a n' hn').leftShift a n hn' = (a * n + a * (a - 1) / 2).negOnePow • γ.shift a - CochainComplex.HomComplex.Cochain.rightShift_leftShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' : ℤ) (hn' : n + a = n'), (γ.leftShift a n' hn').rightShift a n hn' = (a * n' + a * (a - 1) / 2).negOnePow • γ.shift a - CochainComplex.HomComplex.Cochain.δ_shift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a m : ℤ), CochainComplex.HomComplex.δ n m (γ.shift a) = a.negOnePow • (CochainComplex.HomComplex.δ n m γ).shift a - CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain K L n) (a n' n'' : ℤ) (hn' : n' + a = n) (hn'' : n + a = n''), (γ.rightShift a n' hn').leftShift a n hn' = a.negOnePow • (γ.leftShift a n'' hn'').rightShift a n hn'' - CochainComplex.HomComplex.Cochain.leftUnshift_v Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {K L : CochainComplex C ℤ} {n' a : ℤ} (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ) (hn : n + a = n') (p q : ℤ) (hpq : p + n = q) (p' : ℤ) (hp' : p' + n' = q), (γ.leftUnshift n hn).v p q hpq = (a * n' + a * (a - 1) / 2).negOnePow • CategoryTheory.CategoryStruct.comp (K.shiftFunctorObjXIso a p' p ⋯).inv (γ.v p' q ⋯) - CategoryTheory.Pretriangulated.Triangle.shiftFunctor_obj Mathlib.CategoryTheory.Triangulated.TriangleShift
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) (T : CategoryTheory.Pretriangulated.Triangle C), (CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).obj T = CategoryTheory.Pretriangulated.Triangle.mk (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₁) (n.negOnePow • (CategoryTheory.shiftFunctor C n).map T.mor₂) (n.negOnePow • CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map T.mor₃) ((CategoryTheory.shiftFunctorComm C 1 n).hom.app T.obj₁)) - CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₁ Mathlib.CategoryTheory.Triangulated.TriangleShift
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₁ = (CategoryTheory.shiftFunctor C n).map f.hom₁ - CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₂ Mathlib.CategoryTheory.Triangulated.TriangleShift
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₂ = (CategoryTheory.shiftFunctor C n).map f.hom₂ - CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃ Mathlib.CategoryTheory.Triangulated.TriangleShift
∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y), ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₃ = (CategoryTheory.shiftFunctor C n).map f.hom₃ - CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i j k i' j' k' : ℤ) (hi : n + i = i') (hj : n + j = j') (hk : n + k = k') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctor' C n i j k i' j' k' hi hj hk).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).hom - CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₁ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv - CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃ Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
∀ (C : Type u_1) [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ) (hi : n + i = i') (X : CochainComplex C ℤ), ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₃ = n.negOnePow • (HomologicalComplex.XIsoOfEq X ⋯).inv - HomologicalComplex₂.ιTotal_totalFlipIso_f_hom Mathlib.Algebra.Homology.TotalComplexSymmetry
∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c] [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c] [inst_6 : K.flip.HasTotal c] [inst_7 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₂.π c₁ c (i₂, i₁) = j), CategoryTheory.CategoryStruct.comp (K.flip.ιTotal c i₂ i₁ j h) ((K.totalFlipIso c).hom.f j) = c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯ - HomologicalComplex₂.ιTotal_totalFlipIso_f_hom_assoc Mathlib.Algebra.Homology.TotalComplexSymmetry
∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c] [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c] [inst_6 : K.flip.HasTotal c] [inst_7 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₂.π c₁ c (i₂, i₁) = j) {Z : C} (h_1 : (K.total c).X j ⟶ Z), CategoryTheory.CategoryStruct.comp (K.flip.ιTotal c i₂ i₁ j h) (CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).hom.f j) h_1) = CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K.ιTotal c i₁ i₂ j ⋯) h_1 - HomologicalComplex₂.ιTotal_totalFlipIso_f_inv Mathlib.Algebra.Homology.TotalComplexSymmetry
∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c] [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c] [inst_6 : K.flip.HasTotal c] [inst_7 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j), CategoryTheory.CategoryStruct.comp (K.ιTotal c i₁ i₂ j h) ((K.totalFlipIso c).inv.f j) = c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯ - HomologicalComplex₂.ιTotal_totalFlipIso_f_inv_assoc Mathlib.Algebra.Homology.TotalComplexSymmetry
∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{u_5, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c] [inst_3 : TotalComplexShape c₂ c₁ c] [inst_4 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_5 : K.HasTotal c] [inst_6 : K.flip.HasTotal c] [inst_7 : DecidableEq J] (i₁ : I₁) (i₂ : I₂) (j : J) (h : c₁.π c₂ c (i₁, i₂) = j) {Z : C} (h_1 : (K.flip.total c).X j ⟶ Z), CategoryTheory.CategoryStruct.comp (K.ιTotal c i₁ i₂ j h) (CategoryTheory.CategoryStruct.comp ((K.totalFlipIso c).inv.f j) h_1) = CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K.flip.ιTotal c i₂ i₁ j ⋯) h_1 - AbsoluteValue.map_units_int_smul Mathlib.Data.Int.AbsoluteValue
∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : LinearOrderedCommRing S] (abv : AbsoluteValue R S) (x : ℤˣ) (y : R), abv (x • y) = abv y - HNNExtension.NormalWord.group_smul_toList Mathlib.GroupTheory.HNNExtension
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g : G) (w : HNNExtension.NormalWord d), (g • w).toList = w.toList - HNNExtension.NormalWord.t_smul_eq_unitsSMul Mathlib.GroupTheory.HNNExtension
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (w : HNNExtension.NormalWord d), HNNExtension.t • w = HNNExtension.NormalWord.unitsSMul φ 1 w - HNNExtension.NormalWord.t_pow_smul_eq_unitsSMul Mathlib.GroupTheory.HNNExtension
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ℤˣ) (w : HNNExtension.NormalWord d), HNNExtension.t ^ ↑u • w = HNNExtension.NormalWord.unitsSMul φ u w - HNNExtension.NormalWord.smul_cons Mathlib.GroupTheory.HNNExtension
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {d : HNNExtension.NormalWord.TransversalPair G A B} (g₁ g₂ : G) (u : ℤˣ) (w : HNNExtension.NormalWord d) (h1 : w.head ∈ d.set u) (h2 : ∀ u' ∈ Option.map Prod.fst w.toList.head?, w.head ∈ HNNExtension.toSubgroup A B u → u = u'), g₁ • HNNExtension.NormalWord.cons g₂ u w h1 h2 = HNNExtension.NormalWord.cons (g₁ * g₂) u w h1 h2 - HNNExtension.NormalWord.unitsSMul.eq_1 Mathlib.GroupTheory.HNNExtension
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (u : ℤˣ) (w : HNNExtension.NormalWord d), HNNExtension.NormalWord.unitsSMul φ u w = if h : HNNExtension.NormalWord.Cancels u w then HNNExtension.NormalWord.unitsSMulWithCancel φ u w h else let g' := HNNExtension.NormalWord.unitsSMulGroup φ d u w.head; HNNExtension.NormalWord.cons (↑g'.1) u ((↑g'.2 * w.head⁻¹) • w) ⋯ ⋯ - HNNExtension.NormalWord.unitsSMul_one_group_smul Mathlib.GroupTheory.HNNExtension
∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B} (g : ↥A) (w : HNNExtension.NormalWord d), HNNExtension.NormalWord.unitsSMul φ 1 (↑g • w) = ↑(φ g) • HNNExtension.NormalWord.unitsSMul φ 1 w - AlternatingMap.domCoprod.summand_mk'' Mathlib.LinearAlgebra.Alternating.DomCoprod
∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁] [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ] [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : Mᵢ [⋀^ιa]→ₗ[R'] N₁) (b : Mᵢ [⋀^ιb]→ₗ[R'] N₂) (σ : Equiv.Perm (ιa ⊕ ιb)), AlternatingMap.domCoprod.summand a b (Quotient.mk'' σ) = Equiv.Perm.sign σ • MultilinearMap.domDomCongr σ (a.domCoprod ↑b) - MultilinearMap.domCoprod_alternization_coe Mathlib.LinearAlgebra.Alternating.DomCoprod
∀ {ιa : Type u_1} {ιb : Type u_2} [inst : Fintype ιa] [inst_1 : Fintype ιb] {R' : Type u_3} {Mᵢ : Type u_4} {N₁ : Type u_5} {N₂ : Type u_6} [inst_2 : CommSemiring R'] [inst_3 : AddCommGroup N₁] [inst_4 : Module R' N₁] [inst_5 : AddCommGroup N₂] [inst_6 : Module R' N₂] [inst_7 : AddCommMonoid Mᵢ] [inst_8 : Module R' Mᵢ] [inst_9 : DecidableEq ιa] [inst_10 : DecidableEq ιb] (a : MultilinearMap R' (fun x => Mᵢ) N₁) (b : MultilinearMap R' (fun x => Mᵢ) N₂), (MultilinearMap.alternatization a).domCoprod ↑(MultilinearMap.alternatization b) = Finset.univ.sum fun σa => Finset.univ.sum fun σb => Equiv.Perm.sign σa • Equiv.Perm.sign σb • (MultilinearMap.domDomCongr σa a).domCoprod (MultilinearMap.domDomCongr σb b) - TensorProduct.gradedComm_of_tmul_of Mathlib.LinearAlgebra.TensorProduct.Graded.External
∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] (𝒜 : ι → Type u_5) (ℬ : ι → Type u_6) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)] [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)] [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜] [inst_11 : DirectSum.GAlgebra R ℬ] (i j : ι) (a : 𝒜 i) (b : ℬ j), (TensorProduct.gradedComm R 𝒜 ℬ) ((DirectSum.lof R ι 𝒜 i) a ⊗ₜ[R] (DirectSum.lof R ι ℬ j) b) = (-1) ^ (j * i) • (DirectSum.lof R ι ℬ j) b ⊗ₜ[R] (DirectSum.lof R ι 𝒜 i) a - TensorProduct.gradedCommAux_lof_tmul Mathlib.LinearAlgebra.TensorProduct.Graded.External
∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] (𝒜 : ι → Type u_5) (ℬ : ι → Type u_6) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)] [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)] (i j : ι) (a : 𝒜 i) (b : ℬ j), (TensorProduct.gradedCommAux R 𝒜 ℬ) ((DirectSum.lof R (ι × ι) (fun i => TensorProduct R (𝒜 i.1) (ℬ i.2)) (i, j)) (a ⊗ₜ[R] b)) = (-1) ^ (j * i) • (DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) (j, i)) (b ⊗ₜ[R] a) - TensorProduct.gradedCommAux.eq_1 Mathlib.LinearAlgebra.TensorProduct.Graded.External
∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] (𝒜 : ι → Type u_5) (ℬ : ι → Type u_6) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)] [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)], TensorProduct.gradedCommAux R 𝒜 ℬ = DirectSum.toModule R (ι × ι) (DirectSum (ι × ι) fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) fun i => let_fun o := DirectSum.lof R (ι × ι) (fun i => TensorProduct R (ℬ i.1) (𝒜 i.2)) i.swap; let_fun s := (-1) ^ (i.1 * i.2); (s • o) ∘ₗ ↑(TensorProduct.comm R (𝒜 i.1) (ℬ i.2)) - TensorProduct.algebraMap_gradedMul Mathlib.LinearAlgebra.TensorProduct.Graded.External
∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] (𝒜 : ι → Type u_5) (ℬ : ι → Type u_6) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)] [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)] [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜] [inst_11 : DirectSum.GAlgebra R ℬ] (r : R) (x : TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)), ((TensorProduct.gradedMul R 𝒜 ℬ) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1)) x = r • x - TensorProduct.gradedMul_algebraMap Mathlib.LinearAlgebra.TensorProduct.Graded.External
∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] (𝒜 : ι → Type u_5) (ℬ : ι → Type u_6) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)] [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)] [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜] [inst_11 : DirectSum.GAlgebra R ℬ] (x : TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)) (r : R), ((TensorProduct.gradedMul R 𝒜 ℬ) x) ((algebraMap R (DirectSum ι 𝒜)) r ⊗ₜ[R] 1) = r • x - TensorProduct.tmul_of_gradedMul_of_tmul Mathlib.LinearAlgebra.TensorProduct.Graded.External
∀ (R : Type u_1) {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] (𝒜 : ι → Type u_5) (ℬ : ι → Type u_6) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)] [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)] [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜] [inst_11 : DirectSum.GAlgebra R ℬ] (j₁ i₂ : ι) (a₁ : DirectSum ι fun i => 𝒜 i) (b₁ : ℬ j₁) (a₂ : 𝒜 i₂) (b₂ : DirectSum ι fun i => ℬ i), ((TensorProduct.gradedMul R 𝒜 ℬ) (a₁ ⊗ₜ[R] (DirectSum.lof R ι ℬ j₁) b₁)) ((DirectSum.lof R ι 𝒜 i₂) a₂ ⊗ₜ[R] b₂) = (-1) ^ (j₁ * i₂) • (a₁ * (DirectSum.lof R ι 𝒜 i₂) a₂) ⊗ₜ[R] ((DirectSum.lof R ι ℬ j₁) b₁ * b₂) - GradedTensorProduct.lift Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
{R : Type u_1} → {ι : Type u_2} → {A : Type u_3} → {B : Type u_4} → [inst : CommSemiring ι] → [inst_1 : Module ι (Additive ℤˣ)] → [inst_2 : DecidableEq ι] → [inst_3 : CommRing R] → [inst_4 : Ring A] → [inst_5 : Ring B] → [inst_6 : Algebra R A] → [inst_7 : Algebra R B] → (𝒜 : ι → Submodule R A) → (ℬ : ι → Submodule R B) → [inst_8 : GradedAlgebra 𝒜] → [inst_9 : GradedAlgebra ℬ] → {C : Type u_5} → [inst_10 : Ring C] → [inst_11 : Algebra R C] → (f : A →ₐ[R] C) → (g : B →ₐ[R] C) → (∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)) → GradedTensorProduct R 𝒜 ℬ →ₐ[R] C - GradedTensorProduct.tmul_coe_mul_coe_tmul Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] [inst_3 : CommRing R] [inst_4 : Ring A] [inst_5 : Ring B] [inst_6 : Algebra R A] [inst_7 : Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_8 : GradedAlgebra 𝒜] [inst_9 : GradedAlgebra ℬ] {j₁ i₂ : ι} (a₁ : A) (b₁ : ↥(ℬ j₁)) (a₂ : ↥(𝒜 i₂)) (b₂ : B), a₁ ᵍ⊗ₜ[R] ↑b₁ * ↑a₂ ᵍ⊗ₜ[R] b₂ = (-1) ^ (j₁ * i₂) • (a₁ * ↑a₂) ᵍ⊗ₜ[R] (↑b₁ * b₂) - GradedTensorProduct.liftEquiv Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
{R : Type u_1} → {ι : Type u_2} → {A : Type u_3} → {B : Type u_4} → [inst : CommSemiring ι] → [inst_1 : Module ι (Additive ℤˣ)] → [inst_2 : DecidableEq ι] → [inst_3 : CommRing R] → [inst_4 : Ring A] → [inst_5 : Ring B] → [inst_6 : Algebra R A] → [inst_7 : Algebra R B] → (𝒜 : ι → Submodule R A) → (ℬ : ι → Submodule R B) → [inst_8 : GradedAlgebra 𝒜] → [inst_9 : GradedAlgebra ℬ] → {C : Type u_5} → [inst_10 : Ring C] → [inst_11 : Algebra R C] → { fg // ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), fg.1 ↑a * fg.2 ↑b = (-1) ^ (j * i) • (fg.2 ↑b * fg.1 ↑a) } ≃ (GradedTensorProduct R 𝒜 ℬ →ₐ[R] C) - GradedTensorProduct.lift_tmul Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] [inst_3 : CommRing R] [inst_4 : Ring A] [inst_5 : Ring B] [inst_6 : Algebra R A] [inst_7 : Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_8 : GradedAlgebra 𝒜] [inst_9 : GradedAlgebra ℬ] {C : Type u_5} [inst_10 : Ring C] [inst_11 : Algebra R C] (f : A →ₐ[R] C) (g : B →ₐ[R] C) (h_anti_commutes : ∀ ⦃i j : ι⦄ (a : ↥(𝒜 i)) (b : ↥(ℬ j)), f ↑a * g ↑b = (-1) ^ (j * i) • (g ↑b * f ↑a)) (a : A) (b : B), (GradedTensorProduct.lift 𝒜 ℬ f g h_anti_commutes) (a ᵍ⊗ₜ[R] b) = f a * g b - GradedTensorProduct.comm_coe_tmul_coe Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
∀ {R : Type u_1} {ι : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι] [inst_3 : CommRing R] [inst_4 : Ring A] [inst_5 : Ring B] [inst_6 : Algebra R A] [inst_7 : Algebra R B] (𝒜 : ι → Submodule R A) (ℬ : ι → Submodule R B) [inst_8 : GradedAlgebra 𝒜] [inst_9 : GradedAlgebra ℬ] {i j : ι} (a : ↥(𝒜 i)) (b : ↥(ℬ j)), (GradedTensorProduct.comm 𝒜 ℬ) (↑a ᵍ⊗ₜ[R] ↑b) = (-1) ^ (j * i) • ↑b ᵍ⊗ₜ[R] ↑a - CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd Mathlib.LinearAlgebra.CliffordAlgebra.Prod
∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : AddCommGroup N] [inst_4 : Module R M₁] [inst_5 : Module R M₂] [inst_6 : Module R N] {Q₁ : QuadraticForm R M₁} {Q₂ : QuadraticForm R M₂} {Qₙ : QuadraticForm R N} (f₁ : Q₁.Isometry Qₙ) (f₂ : Q₂.Isometry Qₙ), (∀ (x : M₁) (y : M₂), Qₙ.IsOrtho (f₁ x) (f₂ y)) → ∀ (m₁ : CliffordAlgebra Q₁) (m₂ : CliffordAlgebra Q₂) {i₁ i₂ : ZMod 2}, m₁ ∈ CliffordAlgebra.evenOdd Q₁ i₁ → m₂ ∈ CliffordAlgebra.evenOdd Q₂ i₂ → (CliffordAlgebra.map f₁) m₁ * (CliffordAlgebra.map f₂) m₂ = (-1) ^ (i₂ * i₁) • ((CliffordAlgebra.map f₂) m₂ * (CliffordAlgebra.map f₁) m₁) - ContinuousMultilinearMap.alternatization_apply_apply Mathlib.Topology.Algebra.Module.Alternating.Basic
∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N] [inst_7 : TopologicalAddGroup N] [inst_8 : Fintype ι] [inst_9 : DecidableEq ι] (f : ContinuousMultilinearMap R (fun x => M) N) (v : ι → M), (ContinuousMultilinearMap.alternatization f) v = Finset.univ.sum fun σ => Equiv.Perm.sign σ • f (v ∘ ⇑σ) - ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap Mathlib.Topology.Algebra.Module.Alternating.Basic
∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N] [inst_6 : TopologicalSpace N] [inst_7 : TopologicalAddGroup N] [inst_8 : Fintype ι] [inst_9 : DecidableEq ι] (f : ContinuousMultilinearMap R (fun x => M) N), (ContinuousMultilinearMap.alternatization f).toContinuousMultilinearMap = Finset.univ.sum fun σ => Equiv.Perm.sign σ • ContinuousMultilinearMap.domDomCongr σ f
Did you maybe mean
About
Loogle searches of Lean and Mathlib definitions and theorems.
You may also want to try the CLI version, the VS
Code extension, the lean.nvim
integration or the Zulip bot.
Usage
Loogle finds definitions and lemmas in various ways:
By constant:
🔍Real.sin
finds all lemmas whose statement somehow mentions the sine function.By lemma name substring:
🔍"differ"
finds all lemmas that have"differ"
somewhere in their lemma name.By subexpression:
🔍_ * (_ ^ _)
finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.The pattern can also be non-linear, as in
🔍Real.sqrt ?a * Real.sqrt ?a
If the pattern has parameters, they are matched in any order. Both of these will find
List.map
:
🔍(?a -> ?b) -> List ?a -> List ?b
🔍List ?a -> (?a -> ?b) -> List ?b
By main conclusion:
🔍|- tsum _ = _ * tsum _
finds all lemmas where the conclusion (the subexpression to the right of all→
and∀
) has the given shape.As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
🔍|- _ < _ → tsum _ < tsum _
will findtsum_lt_tsum
even though the hypothesisf i < g i
is not the last.
If you pass more than one such search filter, separated by commas
Loogle will return lemmas which match all of them. The
search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
woould find all lemmas which mention the constants Real.sin
and tsum
, have "two"
as a substring of the
lemma name, include a product and a power somewhere in the type,
and have a hypothesis of the form _ < _
(if
there were any such lemmas). Metavariables (?a
) are
assigned independently in each filter.
The #lucky
button will directly send you to the
documentation of the first hit.
Source code
You can find the source code for this service at https://github.com/nomeata/loogle. The https://loogle.lean-lang.org/ service is currently provided by Joachim Breitner <mail@joachim-breitner.de>.
This is Loogle revision fa2ddf5
serving mathlib revision c44d42e