Loogle!

Result

Found 1317 definitions whose name contains "differ". Of these, only the first 200 are shown.

• Ideal.Filtration.Stable.bounded_difference 📋 Mathlib.RingTheory.Filtration
  {R M : Type u} [CommRing R] [AddCommGroup M] [Module R M] {I : Ideal R} {F F' : I.Filtration M} (h : F.Stable) (h' : F'.Stable) (e : F.N 0 = F'.N 0) : ∃ n₀, ∀ (n : ℕ), F.N (n + n₀) ≤ F'.N n ∧ F'.N (n + n₀) ≤ F.N n
• KaehlerDifferential 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Type v
• instAddCommGroupKaehlerDifferential 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : AddCommGroup (Ω[S⁄R])
• instNonemptyKaehlerDifferential 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Nonempty (Ω[S⁄R])
• KaehlerDifferential.kerTotal 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule S (S →₀ S)
• KaehlerDifferential.subsingleton_of_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (h : Function.Surjective ⇑(algebraMap R S)) : Subsingleton (Ω[S⁄R])
• KaehlerDifferential.module' 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {R' : Type u_2} [CommRing R'] [Algebra R' S] [SMulCommClass R R' S] : Module R' (Ω[S⁄R])
• KaehlerDifferential.ideal 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Ideal (TensorProduct R S S)
• KaehlerDifferential.finite 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] : Module.Finite S (Ω[S⁄R])
• KaehlerDifferential.ideal_fg 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] [Algebra.EssFiniteType R S] : (KaehlerDifferential.ideal R S).FG
• KaehlerDifferential.module 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module (TensorProduct R S S) (Ω[S⁄R])
• KaehlerDifferential.DLinearMap 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : S →ₗ[R] Ω[S⁄R]
• KaehlerDifferential.D 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S (Ω[S⁄R])
• Derivation.liftKaehlerDifferential 📋 Mathlib.RingTheory.Kaehler.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : Ω[S⁄R] →ₗ[S] M
• KaehlerDifferential.map 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : Ω[A⁄R] →ₗ[A] Ω[B⁄S]
• KaehlerDifferential.isScalarTower_of_tower 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {R₁ : Type u_2} {R₂ : Type u_3} [CommRing R₁] [CommRing R₂] [Algebra R₁ S] [Algebra R₂ S] [SMul R₁ R₂] [SMulCommClass R R₁ S] [SMulCommClass R R₂ S] [IsScalarTower R₁ R₂ S] : IsScalarTower R₁ R₂ (Ω[S⁄R])
• KaehlerDifferential.map_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (B : Type u_3) [CommRing B] [Algebra S B] [Algebra R B] [IsScalarTower R S B] : Function.Surjective ⇑(KaehlerDifferential.map R S B B)
• KaehlerDifferential.quotKerTotalEquiv 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ((S →₀ S) ⧸ KaehlerDifferential.kerTotal R S) ≃ₗ[S] Ω[S⁄R]
• Derivation.liftKaehlerDifferential_D 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (KaehlerDifferential.D R S).liftKaehlerDifferential = LinearMap.id
• KaehlerDifferential.map_surjective_of_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Surjective ⇑(KaehlerDifferential.map R S A B)
• KaehlerDifferential.mapBaseChange 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : TensorProduct A B (Ω[A⁄R]) →ₗ[B] Ω[B⁄R]
• KaehlerDifferential.span_range_derivation 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) = ⊤
• KaehlerDifferential.derivationQuotKerTotal 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S ((S →₀ S) ⧸ KaehlerDifferential.kerTotal R S)
• KaehlerDifferential.linearMapEquivDerivation 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] : (Ω[S⁄R] →ₗ[S] M) ≃ₗ[S] Derivation R S M
• KaehlerDifferential.span_range_eq_ideal 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Ideal.span (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = KaehlerDifferential.ideal R S
• KaehlerDifferential.kerCotangentToTensor 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] : (RingHom.ker (algebraMap A B)).Cotangent →ₗ[A] TensorProduct A B (Ω[A⁄R])
• KaehlerDifferential.kerToTensor 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] : ↥(RingHom.ker (algebraMap A B)) →ₗ[A] TensorProduct A B (Ω[A⁄R])
• KaehlerDifferential.linearCombination_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Function.Surjective ⇑(Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S))
• KaehlerDifferential.total_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Function.Surjective ⇑(Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S))
• KaehlerDifferential.kerTotal.eq_1 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : KaehlerDifferential.kerTotal R S = Submodule.span S (((Set.range fun x => ((fun₀ | x.1 => 1) + fun₀ | x.2 => 1) - fun₀ | x.1 + x.2 => 1) ∪ Set.range fun x => ((fun₀ | x.2 => x.1) + fun₀ | x.1 => x.2) - fun₀ | x.1 * x.2 => 1) ∪ Set.range fun x => fun₀ | (algebraMap R S) x => 1)
• Derivation.liftKaehlerDifferential_comp_D 📋 Mathlib.RingTheory.Kaehler.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D' : Derivation R S M) (x : S) : D'.liftKaehlerDifferential ((KaehlerDifferential.D R S) x) = D' x
• KaehlerDifferential.isScalarTower' 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower R (TensorProduct R S S) (Ω[S⁄R])
• KaehlerDifferential.kerTotal_eq 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : LinearMap.ker (Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S)) = KaehlerDifferential.kerTotal R S
• instIsScalarTowerTensorProductKaehlerDifferential 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : IsScalarTower S (TensorProduct R S S) (Ω[S⁄R])
• KaehlerDifferential.one_smul_sub_smul_one_mem_ideal 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (a : S) : 1 ⊗ₜ[R] a - a ⊗ₜ[R] 1 ∈ KaehlerDifferential.ideal R S
• KaehlerDifferential.map_D 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] (x : A) : (KaehlerDifferential.map R S A B) ((KaehlerDifferential.D R A) x) = (KaehlerDifferential.D S B) ((algebraMap A B) x)
• KaehlerDifferential.tensorProductTo_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Function.Surjective ⇑(KaehlerDifferential.D R S).tensorProductTo
• KaehlerDifferential.mapBaseChange_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Surjective ⇑(KaehlerDifferential.mapBaseChange R A B)
• KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : S) : ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | 1 => x) = 0
• KaehlerDifferential.kerTotal_mkQ_single_algebraMap 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : R) (y : S) : ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | (algebraMap R S) x => y) = 0
• KaehlerDifferential.exact_mapBaseChange_map 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : Function.Exact ⇑(KaehlerDifferential.mapBaseChange R A B) ⇑(KaehlerDifferential.map R A B B)
• KaehlerDifferential.kerTotal_map' 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (KaehlerDifferential.kerTotal R A ⊔ Submodule.span A (Set.range fun x => fun₀ | (algebraMap R A) x => 1)) = Submodule.restrictScalars A (KaehlerDifferential.kerTotal R B)
• KaehlerDifferential.submodule_span_range_eq_ideal 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Submodule.span S (Set.range fun s => 1 ⊗ₜ[R] s - s ⊗ₜ[R] 1) = Submodule.restrictScalars S (KaehlerDifferential.ideal R S)
• KaehlerDifferential.mapBaseChange_tmul 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (x : B) (y : Ω[A⁄R]) : (KaehlerDifferential.mapBaseChange R A B) (x ⊗ₜ[A] y) = x • (KaehlerDifferential.map R R A B) y
• KaehlerDifferential.fromIdeal 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ↥(KaehlerDifferential.ideal R S) →ₗ[TensorProduct R S S] Ω[S⁄R]
• KaehlerDifferential.kerTotal_map 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] (h : Function.Surjective ⇑(algebraMap A B)) : Submodule.map (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (KaehlerDifferential.kerTotal R A) ⊔ Submodule.span A (Set.range fun x => fun₀ | (algebraMap S B) x => 1) = Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B)
• KaehlerDifferential.linearMapEquivDerivation_apply_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (m : Ω[S⁄R] →ₗ[S] M) (a✝ : S) : ((KaehlerDifferential.linearMapEquivDerivation R S) m) a✝ = m ((KaehlerDifferential.D R S) a✝)
• KaehlerDifferential.kerToTensor_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] (x : ↥(RingHom.ker (algebraMap A B))) : (KaehlerDifferential.kerToTensor R A B) x = 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x
• KaehlerDifferential.linearMapEquivDerivation_symm_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : (KaehlerDifferential.linearMapEquivDerivation R S).symm D = D.liftKaehlerDifferential
• KaehlerDifferential.derivationQuotKerTotal_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x : S) : (KaehlerDifferential.derivationQuotKerTotal R S) x = (KaehlerDifferential.kerTotal R S).mkQ fun₀ | x => 1
• KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S) = (KaehlerDifferential.kerTotal R S).mkQ
• KaehlerDifferential.derivationQuotKerTotal_lift_comp_total 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential ∘ₗ Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S) = (KaehlerDifferential.kerTotal R S).mkQ
• KaehlerDifferential.range_mapBaseChange 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] : LinearMap.range (KaehlerDifferential.mapBaseChange R A B) = LinearMap.ker (KaehlerDifferential.map R A B B)
• KaehlerDifferential.ker_map 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : LinearMap.ker (KaehlerDifferential.map R S A B) = Submodule.map (Finsupp.linearCombination A ⇑(KaehlerDifferential.D R A)) (Submodule.comap (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)) (Submodule.restrictScalars A (KaehlerDifferential.kerTotal S B)))
• KaehlerDifferential.ker_map_of_surjective 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : LinearMap.ker (KaehlerDifferential.map R R A B) = Submodule.map (Finsupp.linearCombination A ⇑(KaehlerDifferential.D R A)) (LinearMap.ker (Finsupp.mapRange.linearMap (Algebra.linearMap A B) ∘ₗ Finsupp.lmapDomain A A ⇑(algebraMap A B)))
• Derivation.liftKaehlerDifferential_comp 📋 Mathlib.RingTheory.Kaehler.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) : D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D
• KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : Function.Exact ⇑(KaehlerDifferential.kerCotangentToTensor R A B) ⇑(KaehlerDifferential.mapBaseChange R A B)
• KaehlerDifferential.kerTotal_mkQ_single_smul 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (r : R) (x y : S) : ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | r • x => y) = r • (KaehlerDifferential.kerTotal R S).mkQ fun₀ | x => y
• KaehlerDifferential.quotKerTotalEquiv_symm_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (a : Ω[S⁄R]) : (KaehlerDifferential.quotKerTotalEquiv R S).symm a = (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential a
• KaehlerDifferential.kerCotangentToTensor_toCotangent 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] (x : ↥(RingHom.ker (algebraMap A B))) : (KaehlerDifferential.kerCotangentToTensor R A B) ((RingHom.ker (algebraMap A B)).toCotangent x) = 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x
• KaehlerDifferential.kerTotal_mkQ_single_add 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x y z : S) : ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | x + y => z) = ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | x => z) + (KaehlerDifferential.kerTotal R S).mkQ fun₀ | y => z
• KaehlerDifferential.kerTotal_mkQ_single_mul 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (x y z : S) : ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | x * y => z) = ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | y => z * x) + (KaehlerDifferential.kerTotal R S).mkQ fun₀ | x => z * y
• KaehlerDifferential.map_compDer 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra S B] [Algebra R B] [IsScalarTower R A B] [IsScalarTower R S B] [SMulCommClass S A B] : (KaehlerDifferential.map R S A B).compDer (KaehlerDifferential.D R A) = Derivation.compAlgebraMap A (Derivation.restrictScalars R (KaehlerDifferential.D S B))
• KaehlerDifferential.range_kerCotangentToTensor 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) [CommRing R] (A : Type u_2) (B : Type u_3) [CommRing A] [CommRing B] [Algebra R A] [Algebra A B] [Algebra R B] [IsScalarTower R A B] (h : Function.Surjective ⇑(algebraMap A B)) : LinearMap.range (KaehlerDifferential.kerCotangentToTensor R A B) = Submodule.restrictScalars A (LinearMap.ker (KaehlerDifferential.mapBaseChange R A B))
• Derivation.liftKaehlerDifferential_unique 📋 Mathlib.RingTheory.Kaehler.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (f f' : Ω[S⁄R] →ₗ[S] M) (hf : f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)) : f = f'
• Derivation.liftKaehlerDifferential_unique_iff 📋 Mathlib.RingTheory.Kaehler.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] {f f' : Ω[S⁄R] →ₗ[S] M} : f = f' ↔ f.compDer (KaehlerDifferential.D R S) = f'.compDer (KaehlerDifferential.D R S)
• KaehlerDifferential.DLinearMap_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (s : S) : (KaehlerDifferential.DLinearMap R S) s = (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, ⋯⟩
• KaehlerDifferential.D_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (s : S) : (KaehlerDifferential.D R S) s = (KaehlerDifferential.ideal R S).toCotangent ⟨1 ⊗ₜ[R] s - s ⊗ₜ[R] 1, ⋯⟩
• KaehlerDifferential.D_tensorProductTo 📋 Mathlib.RingTheory.Kaehler.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (x : ↥(KaehlerDifferential.ideal R S)) : (KaehlerDifferential.D R S).tensorProductTo ↑x = (KaehlerDifferential.ideal R S).toCotangent x
• Derivation.liftKaehlerDifferential_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] {M : Type u_1} [AddCommGroup M] [Module R M] [Module S M] [IsScalarTower R S M] (D : Derivation R S M) (x : ↥(KaehlerDifferential.ideal R S)) : D.liftKaehlerDifferential ((KaehlerDifferential.ideal R S).toCotangent x) = D.tensorProductTo ↑x
• KaehlerDifferential.quotKerTotalEquiv_symm_comp_D 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (↑(KaehlerDifferential.quotKerTotalEquiv R S).symm).compDer (KaehlerDifferential.D R S) = KaehlerDifferential.derivationQuotKerTotal R S
• KaehlerDifferential.quotKerTotalEquiv_apply 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (a✝ : (S →₀ S) ⧸ (KaehlerDifferential.kerTotal R S).toAddSubgroup) : (KaehlerDifferential.quotKerTotalEquiv R S) a✝ = (QuotientAddGroup.lift (KaehlerDifferential.kerTotal R S).toAddSubgroup (Finsupp.linearCombination S ⇑(KaehlerDifferential.D R S)).toAddMonoidHom ⋯) a✝
• KaehlerDifferential.endEquiv 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Module.End S (Ω[S⁄R]) ≃ { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S }
• KaehlerDifferential.quotientCotangentIdeal 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ (KaehlerDifferential.ideal R S).cotangentIdeal) ≃ₐ[S] S
• KaehlerDifferential.quotientCotangentIdealRingEquiv 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : (TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ (KaehlerDifferential.ideal R S).cotangentIdeal ≃+* S
• KaehlerDifferential.End_equiv_aux 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] (f : S →ₐ[R] TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) : (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f = IsScalarTower.toAlgHom R S ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ (KaehlerDifferential.ideal R S).cotangentIdeal) ↔ (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S
• KaehlerDifferential.endEquivAuxEquiv 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : { f // (Ideal.Quotient.mkₐ R (KaehlerDifferential.ideal R S).cotangentIdeal).comp f = IsScalarTower.toAlgHom R S ((TensorProduct R S S ⧸ KaehlerDifferential.ideal R S ^ 2) ⧸ (KaehlerDifferential.ideal R S).cotangentIdeal) } ≃ { f // (Algebra.TensorProduct.lmul' R).kerSquareLift.comp f = AlgHom.id R S }
• KaehlerDifferential.endEquivDerivation' 📋 Mathlib.RingTheory.Kaehler.Basic
  (R : Type u) (S : Type v) [CommRing R] [CommRing S] [Algebra R S] : Derivation R S (Ω[S⁄R]) ≃ₗ[R] Derivation R S ↥(KaehlerDifferential.ideal R S).cotangentIdeal
• CommRingCat.KaehlerDifferential.D 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
  {A B : CommRingCat} (f : A ⟶ B) : (CommRingCat.KaehlerDifferential f).Derivation f
• CommRingCat.KaehlerDifferential 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
  {A B : CommRingCat} (f : A ⟶ B) : ModuleCat ↑B
• CommRingCat.KaehlerDifferential.d 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
  {A B : CommRingCat} {f : A ⟶ B} (b : ↑B) : ↑(CommRingCat.KaehlerDifferential f)
• CommRingCat.KaehlerDifferential.map 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
  {A B A' B' : CommRingCat} {f : A ⟶ B} {f' : A' ⟶ B'} {g : A ⟶ A'} {g' : B ⟶ B'} (fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') : CommRingCat.KaehlerDifferential f ⟶ (ModuleCat.restrictScalars g').obj (CommRingCat.KaehlerDifferential f')
• CommRingCat.KaehlerDifferential.ext 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
  {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} {α β : CommRingCat.KaehlerDifferential f ⟶ M} (h : ∀ (b : ↑B), α (CommRingCat.KaehlerDifferential.d b) = β (CommRingCat.KaehlerDifferential.d b)) : α = β
• CommRingCat.KaehlerDifferential.ext_iff 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
  {A B : CommRingCat} {f : A ⟶ B} {M : ModuleCat ↑B} {α β : CommRingCat.KaehlerDifferential f ⟶ M} : α = β ↔ ∀ (b : ↑B), α (CommRingCat.KaehlerDifferential.d b) = β (CommRingCat.KaehlerDifferential.d b)
• CommRingCat.KaehlerDifferential.map_d 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
  {A B A' B' : CommRingCat} {f : A ⟶ B} {f' : A' ⟶ B'} {g : A ⟶ A'} {g' : B ⟶ B'} (fac : CategoryTheory.CategoryStruct.comp g f' = CategoryTheory.CategoryStruct.comp f g') (b : ↑B) : (CommRingCat.KaehlerDifferential.map fac) (CommRingCat.KaehlerDifferential.d b) = CommRingCat.KaehlerDifferential.d (g' b)
• PresheafOfModules.DifferentialsConstruction.instHasDifferentials 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) : PresheafOfModules.HasDifferentials φ'
• PresheafOfModules.DifferentialsConstruction.derivation' 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').Derivation' φ'
• PresheafOfModules.DifferentialsConstruction.isUniversal' 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) : PresheafOfModules.Derivation.Universal (PresheafOfModules.DifferentialsConstruction.derivation' φ')
• PresheafOfModules.HasDifferentials 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ : S ⟶ F.op.comp R) : Prop
• PresheafOfModules.DifferentialsConstruction.relativeDifferentials' 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))
• PresheafOfModules.HasDifferentials.exists_universal_derivation 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {D : Type u₂} {inst✝¹ : CategoryTheory.Category.{v₂, u₂} D} {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {φ : S ⟶ F.op.comp R} [self : PresheafOfModules.HasDifferentials φ] : ∃ M d, Nonempty d.Universal
• PresheafOfModules.HasDifferentials.mk 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} {F : CategoryTheory.Functor C D} {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} {φ : S ⟶ F.op.comp R} (exists_universal_derivation : ∃ M d, Nonempty d.Universal) : PresheafOfModules.HasDifferentials φ
• PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) (X : Dᵒᵖ) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').obj X = CommRingCat.KaehlerDifferential (φ'.app X)
• PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) {X✝ Y✝ : Dᵒᵖ} (f : X✝ ⟶ Y✝) : (PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f = CommRingCat.KaehlerDifferential.map ⋯
• PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d 📋 Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
  {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] {S' R : CategoryTheory.Functor Dᵒᵖ CommRingCat} (φ' : S' ⟶ R) {X Y : Dᵒᵖ} (f : X ⟶ Y) (x : ↑(R.obj X)) : ((PresheafOfModules.DifferentialsConstruction.relativeDifferentials' φ').map f) (CommRingCat.KaehlerDifferential.d x) = CommRingCat.KaehlerDifferential.d ((R.map f) x)
• CategoryTheory.DifferentialObject 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : Type (max u v)
• CategoryTheory.DifferentialObject.categoryOfDifferentialObjects 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.Category.{v, max u v} (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.obj 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : C
• CategoryTheory.DifferentialObject.Hom 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X Y : CategoryTheory.DifferentialObject S C) : Type v
• CategoryTheory.DifferentialObject.Hom.id 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : X.Hom X
• CategoryTheory.DifferentialObject.forget 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) C
• CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.ConcreteCategory (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.forget_faithful 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : (CategoryTheory.DifferentialObject.forget S C).Faithful
• CategoryTheory.DifferentialObject.instHasForget₂ 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type (u + 1)) [CategoryTheory.LargeCategory C] [CategoryTheory.ConcreteCategory C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.HasForget₂ (CategoryTheory.DifferentialObject S C) C
• CategoryTheory.DifferentialObject.instHasShift 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.HasShift (CategoryTheory.DifferentialObject S C) S
• CategoryTheory.DifferentialObject.hasZeroMorphisms 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] : CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.hasZeroObject 📋 Mathlib.CategoryTheory.DifferentialObject
  (S : Type u_1) [AddMonoidWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroObject C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] : CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.Hom.f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) : X.obj ⟶ Y.obj
• CategoryTheory.DifferentialObject.Hom.comp 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z) : X.Hom Z
• CategoryTheory.DifferentialObject.isoApp 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) : X.obj ≅ Y.obj
• CategoryTheory.DifferentialObject.shiftFunctor 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.Hom.id_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : (CategoryTheory.DifferentialObject.Hom.id X).f = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.DifferentialObject.isoApp_refl 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : CategoryTheory.DifferentialObject.isoApp (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl X.obj
• CategoryTheory.DifferentialObject.d 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : self.obj ⟶ (CategoryTheory.shiftFunctor C 1).obj self.obj
• CategoryTheory.DifferentialObject.instZeroHom 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] {X Y : CategoryTheory.DifferentialObject S C} : Zero (X ⟶ Y)
• CategoryTheory.DifferentialObject.id_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : (CategoryTheory.CategoryStruct.id X).f = CategoryTheory.CategoryStruct.id X.obj
• CategoryTheory.DifferentialObject.Hom.ext 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} {inst✝ : AddMonoidWithOne S} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} {inst✝² : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝³ : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y} (f : x.f = y.f) : x = y
• CategoryTheory.DifferentialObject.Hom.ext_iff 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} {inst✝ : AddMonoidWithOne S} {C : Type u} {inst✝¹ : CategoryTheory.Category.{v, u} C} {inst✝² : CategoryTheory.Limits.HasZeroMorphisms C} {inst✝³ : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y} : x = y ↔ x.f = y.f
• CategoryTheory.DifferentialObject.isoApp_symm 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) : CategoryTheory.DifferentialObject.isoApp f.symm = (CategoryTheory.DifferentialObject.isoApp f).symm
• CategoryTheory.DifferentialObject.isoApp_hom 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) : (CategoryTheory.DifferentialObject.isoApp f).hom = f.hom.f
• CategoryTheory.DifferentialObject.isoApp_inv 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) : (CategoryTheory.DifferentialObject.isoApp f).inv = f.inv.f
• CategoryTheory.DifferentialObject.eqToHom_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (h : X = Y) : (CategoryTheory.eqToHom h).f = CategoryTheory.eqToHom ⋯
• CategoryTheory.DifferentialObject.Hom.comp_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X.Hom Y) (g : Y.Hom Z) : (f.comp g).f = CategoryTheory.CategoryStruct.comp f.f g.f
• CategoryTheory.DifferentialObject.shiftZero 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] : CategoryTheory.DifferentialObject.shiftFunctor C 0 ≅ CategoryTheory.Functor.id (CategoryTheory.DifferentialObject S C)
• CategoryTheory.DifferentialObject.isoApp_trans 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X ≅ Y) (g : Y ≅ Z) : CategoryTheory.DifferentialObject.isoApp (f ≪≫ g) = CategoryTheory.DifferentialObject.isoApp f ≪≫ CategoryTheory.DifferentialObject.isoApp g
• CategoryTheory.DifferentialObject.ext 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B} (w : f.f = g.f := by aesop_cat) : f = g
• CategoryTheory.DifferentialObject.ext_iff 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B} : f = g ↔ autoParam (f.f = g.f) _auto✝
• CategoryTheory.DifferentialObject.comp_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y Z : CategoryTheory.DifferentialObject S C} (f : X ⟶ Y) (g : Y ⟶ Z) : (CategoryTheory.CategoryStruct.comp f g).f = CategoryTheory.CategoryStruct.comp f.f g.f
• CategoryTheory.DifferentialObject.shiftFunctorAdd 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) : CategoryTheory.DifferentialObject.shiftFunctor C (m + n) ≅ (CategoryTheory.DifferentialObject.shiftFunctor C m).comp (CategoryTheory.DifferentialObject.shiftFunctor C n)
• CategoryTheory.DifferentialObject.zero_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [(CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] (P Q : CategoryTheory.DifferentialObject S C) : CategoryTheory.DifferentialObject.Hom.f 0 = 0
• CategoryTheory.DifferentialObject.shiftFunctor_obj_obj 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).obj = (CategoryTheory.shiftFunctor C n).obj X.obj
• CategoryTheory.DifferentialObject.Hom.comm 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map self.f) = CategoryTheory.CategoryStruct.comp self.f Y.d
• CategoryTheory.DifferentialObject.Hom.mk 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ⟶ Y.obj) (comm : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d := by aesop_cat) : X.Hom Y
• CategoryTheory.Functor.mapDifferentialObject 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) : CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S D)
• CategoryTheory.DifferentialObject.mkIso 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : X ≅ Y
• CategoryTheory.DifferentialObject.Hom.comm_assoc 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (self : X.Hom Y) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj Y.obj ⟶ Z) : CategoryTheory.CategoryStruct.comp X.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.f) h) = CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp Y.d h)
• CategoryTheory.DifferentialObject.mkIso_hom_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : (CategoryTheory.DifferentialObject.mkIso f hf).hom.f = f.hom
• CategoryTheory.DifferentialObject.mkIso_inv_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj) (hf : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) = CategoryTheory.CategoryStruct.comp f.hom Y.d) : (CategoryTheory.DifferentialObject.mkIso f hf).inv.f = f.inv
• CategoryTheory.Functor.mapDifferentialObject_obj_obj 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).obj = F.obj X.obj
• CategoryTheory.DifferentialObject.mk 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0 := by aesop_cat) : CategoryTheory.DifferentialObject S C
• CategoryTheory.DifferentialObject.d_squared 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) : CategoryTheory.CategoryStruct.comp self.d ((CategoryTheory.shiftFunctor C 1).map self.d) = 0
• CategoryTheory.DifferentialObject.Hom.mk.injEq 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ⟶ Y.obj) (comm : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d := by aesop_cat) (f✝ : X.obj ⟶ Y.obj) (comm✝ : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f✝) = CategoryTheory.CategoryStruct.comp f✝ Y.d := by aesop_cat) : ({ f := f, comm := comm } = { f := f✝, comm := comm✝ }) = (f = f✝)
• CategoryTheory.DifferentialObject.d_squared_assoc 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (self : CategoryTheory.DifferentialObject S C) {Z : C} (h : (CategoryTheory.shiftFunctor C 1).obj ((CategoryTheory.shiftFunctor C 1).obj self.obj) ⟶ Z) : CategoryTheory.CategoryStruct.comp self.d (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C 1).map self.d) h) = CategoryTheory.CategoryStruct.comp 0 h
• CategoryTheory.Functor.mapDifferentialObject_obj_d 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.Functor.mapDifferentialObject D F η hF).obj X).d = CategoryTheory.CategoryStruct.comp (F.map X.d) (η.app X.obj)
• CategoryTheory.DifferentialObject.shiftFunctor_obj_d 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).obj X).d = CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C n).map X.d) (CategoryTheory.shiftComm X.obj 1 n).hom
• CategoryTheory.DifferentialObject.Hom.mk.sizeOf_spec 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} [SizeOf S] [SizeOf C] (f : X.obj ⟶ Y.obj) (comm : CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d := by aesop_cat) : sizeOf { f := f, comm := comm } = 1 + sizeOf f + sizeOf comm
• CategoryTheory.DifferentialObject.shiftZero_hom_app_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftZero C).hom.app X).f = (CategoryTheory.shiftFunctorZero C S).hom.app X.obj
• CategoryTheory.DifferentialObject.shiftZero_inv_app_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftZero C).inv.app X).f = (CategoryTheory.shiftFunctorZero C S).inv.app X.obj
• CategoryTheory.DifferentialObject.mk.injEq 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0 := by aesop_cat) (obj✝ : C) (d✝ : obj✝ ⟶ (CategoryTheory.shiftFunctor C 1).obj obj✝) (d_squared✝ : CategoryTheory.CategoryStruct.comp d✝ ((CategoryTheory.shiftFunctor C 1).map d✝) = 0 := by aesop_cat) : ({ obj := obj, d := d, d_squared := d_squared } = { obj := obj✝, d := d✝, d_squared := d_squared✝ }) = (obj = obj✝ ∧ HEq d d✝)
• CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).hom.app X).f = (CategoryTheory.shiftFunctorAdd C m n).hom.app X.obj
• CategoryTheory.DifferentialObject.shiftFunctorAdd_inv_app_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (m n : S) (X : CategoryTheory.DifferentialObject S C) : ((CategoryTheory.DifferentialObject.shiftFunctorAdd C m n).inv.app X).f = (CategoryTheory.shiftFunctorAdd C m n).inv.app X.obj
• CategoryTheory.DifferentialObject.mk.sizeOf_spec 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] [SizeOf S] [SizeOf C] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0 := by aesop_cat) : sizeOf { obj := obj, d := d, d_squared := d_squared } = 1 + sizeOf obj + sizeOf d + sizeOf d_squared
• CategoryTheory.DifferentialObject.shiftFunctor_map_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddCommGroupWithOne S] (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (n : S) {X✝ Y✝ : CategoryTheory.DifferentialObject S C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.DifferentialObject.shiftFunctor C n).map f).f = (CategoryTheory.shiftFunctor C n).map f.f
• CategoryTheory.Functor.mapDifferentialObject_map_f 📋 Mathlib.CategoryTheory.DifferentialObject
  {S : Type u_1} [AddMonoidWithOne S] {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] [CategoryTheory.HasShift C S] (D : Type u') [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Limits.HasZeroMorphisms D] [CategoryTheory.HasShift D S] (F : CategoryTheory.Functor C D) (η : (CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) (hF : ∀ (c c' : C), F.map 0 = 0) {X✝ Y✝ : CategoryTheory.DifferentialObject S C} (f : X✝ ⟶ Y✝) : ((CategoryTheory.Functor.mapDifferentialObject D F η hF).map f).f = F.map f.f
• CategoryTheory.DifferentialObject.objEqToHom 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {i j : β} (h : i = j) : X.obj i ⟶ X.obj j
• CategoryTheory.DifferentialObject.objEqToHom_refl 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) (i : β) : X.objEqToHom ⋯ = CategoryTheory.CategoryStruct.id (X.obj i)
• CategoryTheory.DifferentialObject.eqToHom_f' 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (f.f y) = CategoryTheory.CategoryStruct.comp (f.f x) (Y.objEqToHom h)
• CategoryTheory.DifferentialObject.eqToHom_f'_assoc 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) {Z : V} (h✝ : Y.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (f.f y) h✝) = CategoryTheory.CategoryStruct.comp (f.f x) (CategoryTheory.CategoryStruct.comp (Y.objEqToHom h) h✝)
• CategoryTheory.DifferentialObject.objEqToHom_d 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (X.d y) = CategoryTheory.CategoryStruct.comp (X.d x) (X.objEqToHom ⋯)
• CategoryTheory.DifferentialObject.d_squared_apply 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} : CategoryTheory.CategoryStruct.comp (X.d x) (X.d ((fun b_1 => b_1 + { as := 1 }.as • b) x)) = 0
• CategoryTheory.DifferentialObject.objEqToHom_d_assoc 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y) {Z : V} (h✝ : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj y ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (X.d y) h✝) = CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.objEqToHom ⋯) h✝)
• CategoryTheory.DifferentialObject.d_squared_apply_assoc 📋 Mathlib.Algebra.Homology.DifferentialObject
  {β : Type u_1} [AddCommGroup β] {b : β} {V : Type u_2} [CategoryTheory.Category.{u_3, u_2} V] [CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x : β} {Z : V} (h : (CategoryTheory.shiftFunctor (CategoryTheory.GradedObjectWithShift b V) 1).obj X.obj (x + 1 • b) ⟶ Z) : CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.d (x + 1 • b)) h) = CategoryTheory.CategoryStruct.comp 0 h
• Algebra.PreSubmersivePresentation.differential 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) : (P.rels → P.Ring) →ₗ[P.Ring] P.rels → P.Ring
• Algebra.PreSubmersivePresentation.differential.eq_1 📋 Mathlib.RingTheory.Smooth.StandardSmooth
  {R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) : P.differential = (P.basis.constr P.Ring) fun j i => (MvPolynomial.pderiv (P.map i)) (P.relation j)
• CategoryTheory.SingleObj.differenceFunctor 📋 Mathlib.CategoryTheory.SingleObj
  {G : Type u} [Group G] {C : Type v} [CategoryTheory.Category.{w, v} C] (f : C → G) : CategoryTheory.Functor C (CategoryTheory.SingleObj G)
• CategoryTheory.SingleObj.differenceFunctor_obj 📋 Mathlib.CategoryTheory.SingleObj
  {G : Type u} [Group G] {C : Type v} [CategoryTheory.Category.{w, v} C] (f : C → G) (x✝ : C) : (CategoryTheory.SingleObj.differenceFunctor f).obj x✝ = ()
• CategoryTheory.SingleObj.differenceFunctor_map 📋 Mathlib.CategoryTheory.SingleObj
  {G : Type u} [Group G] {C : Type v} [CategoryTheory.Category.{w, v} C] (f : C → G) {x y : C} (x✝ : x ⟶ y) : (CategoryTheory.SingleObj.differenceFunctor f).map x✝ = f y * (f x)⁻¹
• differentiable_id 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Differentiable 𝕜 id
• differentiable_id' 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] : Differentiable 𝕜 fun x => x
• differentiableAt_id 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} : DifferentiableAt 𝕜 id x
• differentiableAt_id' 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} : DifferentiableAt 𝕜 (fun x => x) x
• differentiableOn_id 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {s : Set E} : DifferentiableOn 𝕜 id s
• Differentiable 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : Prop
• DifferentiableAt 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (x : E) : Prop
• differentiableWithinAt_id 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {x : E} {s : Set E} : DifferentiableWithinAt 𝕜 id s x
• DifferentiableOn 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) : Prop
• DifferentiableWithinAt 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (s : Set E) (x : E) : Prop
• differentiable_const 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (c : F) : Differentiable 𝕜 fun x => c
• differentiableAt_const 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} (c : F) : DifferentiableAt 𝕜 (fun x => c) x
• differentiableOn_const 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {s : Set E} (c : F) : DifferentiableOn 𝕜 (fun x => c) s
• differentiableOn_empty 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} : DifferentiableOn 𝕜 f ∅
• differentiableWithinAt_const 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {x : E} {s : Set E} (c : F) : DifferentiableWithinAt 𝕜 (fun x => c) s x
• Set.Subsingleton.differentiableOn 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (hs : s.Subsingleton) : DifferentiableOn 𝕜 f s
• differentiableOn_singleton 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} : DifferentiableOn 𝕜 f {x}
• Differentiable.differentiableAt 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : Differentiable 𝕜 f) : DifferentiableAt 𝕜 f x
• differentiableOn_univ 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} : DifferentiableOn 𝕜 f Set.univ ↔ Differentiable 𝕜 f
• Differentiable.differentiableOn 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : Differentiable 𝕜 f) : DifferentiableOn 𝕜 f s
• Differentiable.eq_1 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  (𝕜 : Type u_1) [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) : Differentiable 𝕜 f = ∀ (x : E), DifferentiableAt 𝕜 f x
• differentiableWithinAt_univ 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} : DifferentiableWithinAt 𝕜 f Set.univ x ↔ DifferentiableAt 𝕜 f x
• DifferentiableAt.differentiableWithinAt 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : DifferentiableAt 𝕜 f x) : DifferentiableWithinAt 𝕜 f s x
• Differentiable.continuous 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} (h : Differentiable 𝕜 f) : Continuous f
• DifferentiableOn.mono 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s t : Set E} (h : DifferentiableOn 𝕜 f t) (st : s ⊆ t) : DifferentiableOn 𝕜 f s
• DifferentiableAt.hasFDerivAt 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : DifferentiableAt 𝕜 f x) : HasFDerivAt f (fderiv 𝕜 f x) x
• DifferentiableWithinAt.insert 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} (h : DifferentiableWithinAt 𝕜 f s x) : DifferentiableWithinAt 𝕜 f (insert x s) x
• differentiableWithinAt_insert_self 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} : DifferentiableWithinAt 𝕜 f (insert x s) x ↔ DifferentiableWithinAt 𝕜 f s x
• DifferentiableAt.continuousAt 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} (h : DifferentiableAt 𝕜 f x) : ContinuousAt f x
• DifferentiableWithinAt.insert' 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} {y : E} : DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 f (insert y s) x
• DifferentiableWithinAt.of_insert 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} {y : E} : DifferentiableWithinAt 𝕜 f (insert y s) x → DifferentiableWithinAt 𝕜 f s x
• differentiableWithinAt_insert 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E} {y : E} : DifferentiableWithinAt 𝕜 f (insert y s) x ↔ DifferentiableWithinAt 𝕜 f s x
• DifferentiableOn.continuousOn 📋 Mathlib.Analysis.Calculus.FDeriv.Basic
  {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : E → F} {s : Set E} (h : DifferentiableOn 𝕜 f s) : ContinuousOn f s

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using (by default) Ctrl-K Ctrl-S. You can also try the #loogle command from LeanSearchClient, the CLI version, the Loogle VS Code extension, the lean.nvim integration or the Zulip bot.

Usage

Loogle finds definitions and lemmas in various ways:

1. By constant:
   🔍 Real.sin
   finds all lemmas whose statement somehow mentions the sine function.

2. By lemma name substring:
   🔍 "differ"
   finds all lemmas that have "differ" somewhere in their lemma name.

3. 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

4. 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 find tsum_lt_tsum even though the hypothesis f 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 provided by the Lean FRO.

This is Loogle revision 4e1aab0 serving mathlib revision 79ca167