Loogle!
Result
Found 1167 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} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {I : Ideal R} {F F' : I.Filtration M}, F.Stable → F'.Stable → 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) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst : Algebra R S] → Type v - instAddCommGroupKaehlerDifferential Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → AddCommGroup (Ω[S⁄R]) - instNonemptyKaehlerDifferential Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S], Nonempty (Ω[S⁄R]) - KaehlerDifferential.kerTotal Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst : Algebra R S] → Submodule S (S →₀ S) - KaehlerDifferential.subsingleton_of_surjective Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S], Function.Surjective ⇑(algebraMap R S) → Subsingleton (Ω[S⁄R]) - KaehlerDifferential.module' Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {R' : Type u_2} → [inst_3 : CommRing R'] → [inst_4 : Algebra R' S] → [inst_5 : SMulCommClass R R' S] → Module R' (Ω[S⁄R]) - KaehlerDifferential.ideal Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Ideal (TensorProduct R S S) - KaehlerDifferential.finite Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : Algebra.EssFiniteType R S], Module.Finite S (Ω[S⁄R]) - KaehlerDifferential.ideal_fg Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : Algebra.EssFiniteType R S], (KaehlerDifferential.ideal R S).FG - KaehlerDifferential.module Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Module (TensorProduct R S S) (Ω[S⁄R]) - KaehlerDifferential.DLinearMap Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → S →ₗ[R] Ω[S⁄R] - KaehlerDifferential.D Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Derivation R S (Ω[S⁄R]) - Derivation.liftKaehlerDifferential Mathlib.RingTheory.Kaehler.Basic
{R : Type u} → {S : Type v} → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {M : Type u_1} → [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → [inst_5 : Module S M] → [inst_6 : IsScalarTower R S M] → Derivation R S M → Ω[S⁄R] →ₗ[S] M - KaehlerDifferential.map Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → (A : Type u_2) → (B : Type u_3) → [inst_3 : CommRing A] → [inst_4 : CommRing B] → [inst_5 : Algebra R A] → [inst_6 : Algebra A B] → [inst_7 : Algebra S B] → [inst_8 : Algebra R B] → [inst_9 : IsScalarTower R A B] → [inst_10 : IsScalarTower R S B] → [inst_11 : SMulCommClass S A B] → Ω[A⁄R] →ₗ[A] Ω[B⁄S] - KaehlerDifferential.isScalarTower_of_tower Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {R₁ : Type u_2} {R₂ : Type u_3} [inst_3 : CommRing R₁] [inst_4 : CommRing R₂] [inst_5 : Algebra R₁ S] [inst_6 : Algebra R₂ S] [inst_7 : SMul R₁ R₂] [inst_8 : SMulCommClass R R₁ S] [inst_9 : SMulCommClass R R₂ S] [inst_10 : IsScalarTower R₁ R₂ S], IsScalarTower R₁ R₂ (Ω[S⁄R]) - KaehlerDifferential.map_surjective Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (B : Type u_3) [inst_3 : CommRing B] [inst_4 : Algebra S B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R S B], Function.Surjective ⇑(KaehlerDifferential.map R S B B) - KaehlerDifferential.quotKerTotalEquiv Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2) (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B] [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B] [inst_11 : SMulCommClass S A B], Function.Surjective ⇑(algebraMap A B) → Function.Surjective ⇑(KaehlerDifferential.map R S A B) - KaehlerDifferential.mapBaseChange Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → [inst : CommRing R] → (A : Type u_2) → (B : Type u_3) → [inst_1 : CommRing A] → [inst_2 : CommRing B] → [inst_3 : Algebra R A] → [inst_4 : Algebra A B] → [inst_5 : Algebra R B] → [inst_6 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S], Submodule.span S (Set.range ⇑(KaehlerDifferential.D R S)) = ⊤ - KaehlerDifferential.derivationQuotKerTotal Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Derivation R S ((S →₀ S) ⧸ KaehlerDifferential.kerTotal R S) - KaehlerDifferential.linearMapEquivDerivation Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → (S : Type v) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → {M : Type u_1} → [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → [inst_5 : Module S M] → [inst_6 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) → [inst : CommRing R] → (A : Type u_2) → (B : Type u_3) → [inst_1 : CommRing A] → [inst_2 : CommRing B] → [inst_3 : Algebra R A] → [inst_4 : Algebra A B] → (RingHom.ker (algebraMap A B)).Cotangent →ₗ[A] TensorProduct A B (Ω[A⁄R]) - KaehlerDifferential.kerToTensor Mathlib.RingTheory.Kaehler.Basic
(R : Type u) → [inst : CommRing R] → (A : Type u_2) → (B : Type u_3) → [inst_1 : CommRing A] → [inst_2 : CommRing B] → [inst_3 : Algebra R A] → [inst_4 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1} [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S], IsScalarTower R (TensorProduct R S S) (Ω[S⁄R]) - KaehlerDifferential.kerTotal_eq Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2) (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B] [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B] [inst_11 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S], Function.Surjective ⇑(KaehlerDifferential.D R S).tensorProductTo - KaehlerDifferential.mapBaseChange_surjective Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B], 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : R) (y : S), ((KaehlerDifferential.kerTotal R S).mkQ fun₀ | (algebraMap R S) x => y) = 0 - KaehlerDifferential.linearMapEquivDerivation_apply_apply Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1} [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (m : Ω[S⁄R] →ₗ[S] M) (a : S), ((KaehlerDifferential.linearMapEquivDerivation R S) m) a = m ((KaehlerDifferential.D R S) a) - KaehlerDifferential.exact_mapBaseChange_map Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B], Function.Exact ⇑(KaehlerDifferential.mapBaseChange R A B) ⇑(KaehlerDifferential.map R A B B) - KaehlerDifferential.linearMapEquivDerivation_symm_apply Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1} [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (D : Derivation R S M), (KaehlerDifferential.linearMapEquivDerivation R S).symm D = D.liftKaehlerDifferential - KaehlerDifferential.kerTotal_map' Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B], 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : 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) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2) (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B] [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B], 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.kerToTensor_apply Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] (x : ↥(RingHom.ker (algebraMap A B))), (KaehlerDifferential.kerToTensor R A B) x = 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x - KaehlerDifferential.derivationQuotKerTotal_apply Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2) (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B] [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B] [inst_11 : 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) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B], 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} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1} [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (D : Derivation R S M), D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D - KaehlerDifferential.quotKerTotalEquiv_symm_apply Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (a : Ω[S⁄R]), (KaehlerDifferential.quotKerTotalEquiv R S).symm a = (KaehlerDifferential.derivationQuotKerTotal R S).liftKaehlerDifferential a - KaehlerDifferential.exact_kerCotangentToTensor_mapBaseChange Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B], 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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.kerCotangentToTensor_toCotangent Mathlib.RingTheory.Kaehler.Basic
∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (A : Type u_2) (B : Type u_3) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra A B] [inst_7 : Algebra S B] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B] [inst_11 : 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) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [inst_6 : IsScalarTower R A B], 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} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1} [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] (f f' : Ω[S⁄R] →ₗ[S] M), 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} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1} [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1} [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : 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) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : 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) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : 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) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : 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) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : 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) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : 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} → (A ⟶ B) → ModuleCat ↑B - CommRingCat.KaehlerDifferential.d Mathlib.Algebra.Category.ModuleCat.Differentials.Basic
{A B : CommRingCat} → {f : A ⟶ 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'} → 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}, (∀ (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₂} [inst : 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₂} → [inst : 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₂} → [inst : 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₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {D : Type u₂} → [inst_1 : 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₂} → [inst : 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_1 : 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₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : 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}, (∃ M d, Nonempty d.Universal) → PresheafOfModules.HasDifferentials φ - PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
∀ {D : Type u₂} [inst : 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₂} [inst : 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₂} [inst : 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) → [inst : AddMonoidWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst : CategoryTheory.HasShift C S] → Type (max u v) - CategoryTheory.DifferentialObject.categoryOfDifferentialObjects Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.Category.{v, max u v} (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.obj Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.DifferentialObject S C → C - CategoryTheory.DifferentialObject.Hom Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.DifferentialObject S C → CategoryTheory.DifferentialObject S C → Type v - CategoryTheory.DifferentialObject.Hom.id Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → (X : CategoryTheory.DifferentialObject S C) → X.Hom X - CategoryTheory.DifferentialObject.forget Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) → [inst : AddMonoidWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) C - CategoryTheory.DifferentialObject.concreteCategoryOfDifferentialObjects Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) → [inst : AddMonoidWithOne S] → (C : Type (u + 1)) → [inst_1 : CategoryTheory.LargeCategory C] → [inst_2 : CategoryTheory.ConcreteCategory C] → [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_4 : CategoryTheory.HasShift C S] → CategoryTheory.ConcreteCategory (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.forget_faithful Mathlib.CategoryTheory.DifferentialObject
∀ (S : Type u_1) [inst : AddMonoidWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S], (CategoryTheory.DifferentialObject.forget S C).Faithful - CategoryTheory.DifferentialObject.instHasForget₂ Mathlib.CategoryTheory.DifferentialObject
(S : Type u_1) → [inst : AddMonoidWithOne S] → (C : Type (u + 1)) → [inst_1 : CategoryTheory.LargeCategory C] → [inst_2 : CategoryTheory.ConcreteCategory C] → [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_4 : CategoryTheory.HasShift C S] → CategoryTheory.HasForget₂ (CategoryTheory.DifferentialObject S C) C - CategoryTheory.DifferentialObject.instHasShift Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddCommGroupWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → CategoryTheory.HasShift (CategoryTheory.DifferentialObject S C) S - CategoryTheory.DifferentialObject.hasZeroMorphisms Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → [inst_4 : (CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms] → CategoryTheory.Limits.HasZeroMorphisms (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.hasZeroObject Mathlib.CategoryTheory.DifferentialObject
∀ (S : Type u_1) [inst : AddMonoidWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_4 : CategoryTheory.HasShift C S] [inst_5 : (CategoryTheory.shiftFunctor C 1).PreservesZeroMorphisms], CategoryTheory.Limits.HasZeroObject (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.Hom.f Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y : CategoryTheory.DifferentialObject S C} → X.Hom Y → (X.obj ⟶ Y.obj) - CategoryTheory.DifferentialObject.Hom.comp Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y Z : CategoryTheory.DifferentialObject S C} → X.Hom Y → Y.Hom Z → X.Hom Z - CategoryTheory.DifferentialObject.isoApp Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y : CategoryTheory.DifferentialObject S C} → (X ≅ Y) → (X.obj ≅ Y.obj) - CategoryTheory.DifferentialObject.shiftFunctor Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddCommGroupWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → S → CategoryTheory.Functor (CategoryTheory.DifferentialObject S C) (CategoryTheory.DifferentialObject S C) - CategoryTheory.DifferentialObject.Hom.id_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : 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} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → [inst_4 : (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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : CategoryTheory.HasShift C S} {X Y : CategoryTheory.DifferentialObject S C} {x y : X.Hom Y}, 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_1 : CategoryTheory.Category.{v, u} C} {inst_2 : CategoryTheory.Limits.HasZeroMorphisms C} {inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} → [inst : AddCommGroupWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {A B : CategoryTheory.DifferentialObject S C} {f g : A ⟶ B}, autoParam (f.f = g.f) _auto✝ → f = g - CategoryTheory.DifferentialObject.ext_iff Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} → [inst : AddCommGroupWithOne S] → (C : Type u) → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] [inst_4 : (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} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y : CategoryTheory.DifferentialObject S C} → (f : X.obj ⟶ Y.obj) → autoParam (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d) _auto✝ → X.Hom Y - CategoryTheory.Functor.mapDifferentialObject Mathlib.CategoryTheory.DifferentialObject
{S : Type u_1} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → (D : Type u') → [inst_4 : CategoryTheory.Category.{v', u'} D] → [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] → [inst_6 : CategoryTheory.HasShift D S] → (F : CategoryTheory.Functor C D) → ((CategoryTheory.shiftFunctor C 1).comp F ⟶ F.comp (CategoryTheory.shiftFunctor D 1)) → (∀ (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} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → {X Y : CategoryTheory.DifferentialObject S C} → (f : X.obj ≅ Y.obj) → 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u') [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] [inst_6 : 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} → [inst : AddMonoidWithOne S] → {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] → [inst_3 : CategoryTheory.HasShift C S] → (obj : C) → (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) → autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0) _auto✝ → CategoryTheory.DifferentialObject S C - CategoryTheory.DifferentialObject.d_squared Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ⟶ Y.obj) (comm : autoParam (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d) _auto✝) (f_1 : X.obj ⟶ Y.obj) (comm_1 : autoParam (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f_1) = CategoryTheory.CategoryStruct.comp f_1 Y.d) _auto✝), ({ f := f, comm := comm } = { f := f_1, comm := comm_1 }) = (f = f_1) - CategoryTheory.DifferentialObject.d_squared_assoc Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u') [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] [inst_6 : 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} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] {X Y : CategoryTheory.DifferentialObject S C} [inst_4 : SizeOf S] [inst_5 : SizeOf C] (f : X.obj ⟶ Y.obj) (comm : autoParam (CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f) = CategoryTheory.CategoryStruct.comp f Y.d) _auto✝), sizeOf { f := f, comm := comm } = 1 + sizeOf f + sizeOf comm - CategoryTheory.DifferentialObject.shiftZero_hom_app_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0) _auto✝) (obj_1 : C) (d_1 : obj_1 ⟶ (CategoryTheory.shiftFunctor C 1).obj obj_1) (d_squared_1 : autoParam (CategoryTheory.CategoryStruct.comp d_1 ((CategoryTheory.shiftFunctor C 1).map d_1) = 0) _auto✝), ({ obj := obj, d := d, d_squared := d_squared } = { obj := obj_1, d := d_1, d_squared := d_squared_1 }) = (obj = obj_1 ∧ HEq d d_1) - CategoryTheory.DifferentialObject.shiftFunctorAdd_hom_app_f Mathlib.CategoryTheory.DifferentialObject
∀ {S : Type u_1} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] [inst_4 : SizeOf S] [inst_5 : SizeOf C] (obj : C) (d : obj ⟶ (CategoryTheory.shiftFunctor C 1).obj obj) (d_squared : autoParam (CategoryTheory.CategoryStruct.comp d ((CategoryTheory.shiftFunctor C 1).map d) = 0) _auto✝), 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} [inst : AddCommGroupWithOne S] (C : Type u) [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : 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} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S] (D : Type u') [inst_4 : CategoryTheory.Category.{v', u'} D] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D] [inst_6 : 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} → [inst : AddCommGroup β] → {b : β} → {V : Type u_2} → [inst_1 : CategoryTheory.Category.{u_3, u_2} V] → [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] → (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) → {i j : β} → i = j → (X.obj i ⟶ X.obj j) - CategoryTheory.DifferentialObject.objEqToHom_refl Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : 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} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : 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} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] {X Y : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)} (f : X ⟶ Y) {x y : β} (h : x = y) {Z : V} (h_1 : Y.obj y ⟶ Z), CategoryTheory.CategoryStruct.comp (X.objEqToHom h) (CategoryTheory.CategoryStruct.comp (f.f y) h_1) = CategoryTheory.CategoryStruct.comp (f.f x) (CategoryTheory.CategoryStruct.comp (Y.objEqToHom h) h_1) - CategoryTheory.DifferentialObject.objEqToHom_d Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : 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} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : 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} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms V] (X : CategoryTheory.DifferentialObject ℤ (CategoryTheory.GradedObjectWithShift b V)) {x y : β} (h : x = y) {Z : V} (h_1 : (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_1) = CategoryTheory.CategoryStruct.comp (X.d x) (CategoryTheory.CategoryStruct.comp (X.objEqToHom ⋯) h_1) - CategoryTheory.DifferentialObject.d_squared_apply_assoc Mathlib.Algebra.Homology.DifferentialObject
∀ {β : Type u_1} [inst : AddCommGroup β] {b : β} {V : Type u_2} [inst_1 : CategoryTheory.Category.{u_3, u_2} V] [inst_2 : 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 - CategoryTheory.SingleObj.differenceFunctor Mathlib.CategoryTheory.SingleObj
{G : Type u} → [inst : Group G] → {C : Type v} → [inst_1 : CategoryTheory.Category.{w, v} C] → (C → G) → CategoryTheory.Functor C (CategoryTheory.SingleObj G) - CategoryTheory.SingleObj.differenceFunctor_obj Mathlib.CategoryTheory.SingleObj
∀ {G : Type u} [inst : Group G] {C : Type v} [inst_1 : 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} [inst : Group G] {C : Type v} [inst_1 : CategoryTheory.Category.{w, v} C] (f : C → G) {x y : C} (x_1 : x ⟶ y), (CategoryTheory.SingleObj.differenceFunctor f).map x_1 = f y * (f x)⁻¹ - differentiable_id Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], Differentiable 𝕜 id - differentiable_id' Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E], Differentiable 𝕜 fun x => x - differentiableAt_id Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E}, DifferentiableAt 𝕜 id x - differentiableAt_id' Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E}, DifferentiableAt 𝕜 (fun x => x) x - differentiableOn_id Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {s : Set E}, DifferentiableOn 𝕜 id s - Differentiable Mathlib.Analysis.Calculus.FDeriv.Basic
(𝕜 : Type u_1) → [inst : NontriviallyNormedField 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [inst : NormedSpace 𝕜 F] → (E → F) → Prop - DifferentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
(𝕜 : Type u_1) → [inst : NontriviallyNormedField 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [inst : NormedSpace 𝕜 F] → (E → F) → E → Prop - differentiableWithinAt_id Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 id s x - DifferentiableOn Mathlib.Analysis.Calculus.FDeriv.Basic
(𝕜 : Type u_1) → [inst : NontriviallyNormedField 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [inst : NormedSpace 𝕜 F] → (E → F) → Set E → Prop - DifferentiableWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
(𝕜 : Type u_1) → [inst : NontriviallyNormedField 𝕜] → {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace 𝕜 E] → {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [inst : NormedSpace 𝕜 F] → (E → F) → Set E → E → Prop - differentiable_const Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (c : F), Differentiable 𝕜 fun x => c - differentiableAt_const Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} (c : F), DifferentiableAt 𝕜 (fun x => c) x - differentiableOn_const Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E} (c : F), DifferentiableOn 𝕜 (fun x => c) s - differentiableOn_empty Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, DifferentiableOn 𝕜 f ∅ - differentiableWithinAt_const Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : 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} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, s.Subsingleton → DifferentiableOn 𝕜 f s - differentiableOn_singleton Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, DifferentiableOn 𝕜 f {x} - Differentiable.differentiableAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, Differentiable 𝕜 f → DifferentiableAt 𝕜 f x - differentiableOn_univ Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, DifferentiableOn 𝕜 f Set.univ ↔ Differentiable 𝕜 f - Differentiable.differentiableOn Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, Differentiable 𝕜 f → DifferentiableOn 𝕜 f s - Differentiable.eq_1 Mathlib.Analysis.Calculus.FDeriv.Basic
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F), Differentiable 𝕜 f = ∀ (x : E), DifferentiableAt 𝕜 f x - differentiableWithinAt_univ Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : 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} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableAt 𝕜 f x → DifferentiableWithinAt 𝕜 f s x - Differentiable.continuous Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}, Differentiable 𝕜 f → Continuous f - DifferentiableOn.mono Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s t : Set E}, DifferentiableOn 𝕜 f t → s ⊆ t → DifferentiableOn 𝕜 f s - DifferentiableAt.hasFDerivAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, DifferentiableAt 𝕜 f x → HasFDerivAt f (fderiv 𝕜 f x) x - DifferentiableAt.continuousAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E}, DifferentiableAt 𝕜 f x → ContinuousAt f x - DifferentiableOn.continuousOn Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}, DifferentiableOn 𝕜 f s → ContinuousOn f s - DifferentiableOn.eq_1 Mathlib.Analysis.Calculus.FDeriv.Basic
∀ (𝕜 : Type u_1) [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F) (s : Set E), DifferentiableOn 𝕜 f s = ∀ x ∈ s, DifferentiableWithinAt 𝕜 f s x - DifferentiableWithinAt.mono Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s t : Set E}, DifferentiableWithinAt 𝕜 f t x → s ⊆ t → DifferentiableWithinAt 𝕜 f s x - DifferentiableWithinAt.continuousWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → ContinuousWithinAt f s x - DifferentiableWithinAt.hasFDerivWithinAt Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {x : E} {s : Set E}, DifferentiableWithinAt 𝕜 f s x → HasFDerivWithinAt f (fderivWithin 𝕜 f s x) s x - DifferentiableOn.congr Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {s : Set E}, DifferentiableOn 𝕜 f s → (∀ x ∈ s, f₁ x = f x) → DifferentiableOn 𝕜 f₁ s - differentiableOn_congr Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {s : Set E}, (∀ x ∈ s, f₁ x = f x) → (DifferentiableOn 𝕜 f₁ s ↔ DifferentiableOn 𝕜 f s) - DifferentiableAt.congr_of_eventuallyEq Mathlib.Analysis.Calculus.FDeriv.Basic
∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f f₁ : E → F} {x : E}, DifferentiableAt 𝕜 f x → f₁ =ᶠ[nhds x] f → DifferentiableAt 𝕜 f₁ x
About
Loogle searches Lean and Mathlib definitions and theorems.
You can use Loogle from witin the Lean4 VSCode language extension
using (by default) Ctrl-K Ctrl-S. You can also try 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:
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 provided by the Lean FRO.
This is Loogle revision f46663a
serving mathlib revision c9428b0