Loogle!

Result

Found 115 declarations mentioning List.TFAE.

• List.TFAE 📋 Mathlib.Data.List.TFAE
  (l : List Prop) : Prop
• List.tfae_nil 📋 Mathlib.Data.List.TFAE
  : [].TFAE
• List.tfae_singleton 📋 Mathlib.Data.List.TFAE
  (p : Prop) : [p].TFAE
• List.tfae_reverse 📋 Mathlib.Data.List.TFAE
  {l : List Prop} : l.reverse.TFAE ↔ l.TFAE
• List.TFAE.not 📋 Mathlib.Data.List.TFAE
  {l : List Prop} : l.TFAE → (List.map Not l).TFAE
• List.tfae_not_iff 📋 Mathlib.Data.List.TFAE
  {l : List Prop} : (List.map Not l).TFAE ↔ l.TFAE
• List.Perm.tfae_iff 📋 Mathlib.Data.List.TFAE
  {l₁ l₂ : List Prop} (h : l₁.Perm l₂) : l₁.TFAE ↔ l₂.TFAE
• List.TFAE.subset 📋 Mathlib.Data.List.TFAE
  {l₁ l₂ : List Prop} (h : l₂.TFAE) (hl : l₁ ⊆ l₂) : l₁.TFAE
• List.tfae_of_forall 📋 Mathlib.Data.List.TFAE
  {b : Prop} {l : List Prop} (h : ∀ a ∈ l, a ↔ b) : l.TFAE
• List.tfae_congr 📋 Mathlib.Data.List.TFAE
  {l₁ l₂ : List Prop} (h₁₂ : l₁ ⊆ l₂) (h₂₁ : l₂ ⊆ l₁) : l₁.TFAE ↔ l₂.TFAE
• List.forall_tfae 📋 Mathlib.Data.List.TFAE
  {α : Type u_1} (l : List (α → Prop)) (H : ∀ (a : α), (List.map (fun p => p a) l).TFAE) : (List.map (fun p => ∀ (a : α), p a) l).TFAE
• List.exists_tfae 📋 Mathlib.Data.List.TFAE
  {α : Type u_1} (l : List (α → Prop)) (H : ∀ (a : α), (List.map (fun p => p a) l).TFAE) : (List.map (fun p => ∃ a, p a) l).TFAE
• List.TFAE.out 📋 Mathlib.Data.List.TFAE
  {l : List Prop} (h : l.TFAE) (i j : ℕ) {a b : Prop} (h₁ : l[i - 1]? = some a := by rfl) (h₂ : l[j - 1]? = some b := by rfl) : autoParam (i ≠ 0) List.TFAE.out._auto_5 → autoParam (j ≠ 0) List.TFAE.out._auto_7 → (a ↔ b)
• List.tfae_iff_pairwise 📋 Mathlib.Data.List.Pairwise
  {l : List Prop} : l.TFAE ↔ List.Pairwise (fun x1 x2 => x1 ↔ x2) l
• List.tfae_cons_self 📋 Mathlib.Data.List.Pairwise
  {a : Prop} {l : List Prop} : (a :: a :: l).TFAE ↔ (a :: l).TFAE
• List.tfae_cons_of_mem 📋 Mathlib.Data.List.Pairwise
  {a : Prop} {l : List Prop} (h : a ∈ l) : (a :: l).TFAE ↔ l.TFAE
• List.tfae_cons_cons 📋 Mathlib.Data.List.Pairwise
  {a b : Prop} {l : List Prop} : (a :: b :: l).TFAE ↔ (a ↔ b) ∧ (b :: l).TFAE
• List.tfae_cons 📋 Mathlib.Data.List.Pairwise
  {a b : Prop} {l : List Prop} (h : b ∈ l) : (a :: l).TFAE ↔ (a ↔ b) ∧ l.TFAE
• List.tfae_of_cycle 📋 Mathlib.Data.List.Pairwise
  {a b : Prop} {l : List Prop} (h_chain : List.IsChain (fun x1 x2 => x1 → x2) (a :: b :: l)) (h_last : l.getLastD b → a) : (a :: b :: l).TFAE
• List.tfae_concat_of_mem 📋 Mathlib.Data.List.Pairwise
  {a : Prop} {l : List Prop} (h : a ∈ l) : (l ++ [a]).TFAE ↔ l.TFAE
• List.tfae_concat 📋 Mathlib.Data.List.Pairwise
  {a b : Prop} {l : List Prop} (h : b ∈ l) : (l ++ [a]).TFAE ↔ (a ↔ b) ∧ l.TFAE
• List.tfae_append 📋 Mathlib.Data.List.Pairwise
  {l₁ l₂ : List Prop} : (l₁ ++ l₂).TFAE ↔ l₁.TFAE ∧ l₂.TFAE ∧ ∀ a ∈ l₁, ∀ b ∈ l₂, a ↔ b
• List.tfae_append_of_mem 📋 Mathlib.Data.List.Pairwise
  {a b : Prop} {l₁ l₂ : List Prop} (ha : a ∈ l₁) (hb : b ∈ l₂) : (l₁ ++ l₂).TFAE ↔ (a ↔ b) ∧ l₁.TFAE ∧ l₂.TFAE
• noZeroDivisors_tfae 📋 Mathlib.Algebra.Ring.Basic
  {R : Type u_3} [NonUnitalNonAssocRing R] : [NoZeroDivisors R, IsLeftCancelMulZero R, IsRightCancelMulZero R, IsCancelMulZero R].TFAE
• Set.WellFoundedOn.acc_iff_wellFoundedOn 📋 Mathlib.Order.WellFoundedSet
  {α : Type u_6} {r : α → α → Prop} {a : α} : [Acc r a, {b | Relation.ReflTransGen r b a}.WellFoundedOn r, {b | Relation.TransGen r b a}.WellFoundedOn r].TFAE
• CompleteLattice.wellFoundedGT_characterisations 📋 Mathlib.Order.CompactlyGenerated.Basic
  (α : Type u_2) [CompleteLattice α] : [WellFoundedGT α, CompleteLattice.IsSupFiniteCompact α, CompleteLattice.IsSupClosedCompact α, ∀ (k : α), IsCompactElement k].TFAE
• Function.Exact.split_tfae 📋 Mathlib.Algebra.Exact.Basic
  {R : Type u_8} {M : Type u_9} {N : Type u_10} {P : Type u_11} [Semiring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) (hf : Function.Injective ⇑f) (hg : Function.Surjective ⇑g) : [∃ l, g ∘ₗ l = LinearMap.id, ∃ l, l ∘ₗ f = LinearMap.id, ∃ e, f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e].TFAE
• Function.Exact.split_tfae' 📋 Mathlib.Algebra.Exact.Basic
  {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [Semiring R] [AddCommGroup M] [AddCommGroup N] [AddCommGroup P] [Module R M] [Module R N] [Module R P] {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : Function.Exact ⇑f ⇑g) : [Function.Injective ⇑f ∧ ∃ l, g ∘ₗ l = LinearMap.id, Function.Surjective ⇑g ∧ ∃ l, l ∘ₗ f = LinearMap.id, ∃ e, f = ↑e.symm ∘ₗ LinearMap.inl R M P ∧ g = LinearMap.snd R M P ∘ₗ ↑e].TFAE
• Ideal.isCoprime_tfae 📋 Mathlib.RingTheory.Ideal.Operations
  {R : Type u} [CommSemiring R] {I J : Ideal R} : [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE
• IsLocalRing.local_hom_TFAE 📋 Mathlib.RingTheory.LocalRing.RingHom.Basic
  {R : Type u_1} {S : Type u_2} [CommSemiring R] [IsLocalRing R] [CommSemiring S] [IsLocalRing S] (f : R →+* S) : [IsLocalHom f, ⇑f '' ↑(IsLocalRing.maximalIdeal R) ⊆ ↑(IsLocalRing.maximalIdeal S), Ideal.map f (IsLocalRing.maximalIdeal R) ≤ IsLocalRing.maximalIdeal S, IsLocalRing.maximalIdeal R ≤ Ideal.comap f (IsLocalRing.maximalIdeal S), Ideal.comap f (IsLocalRing.maximalIdeal S) = IsLocalRing.maximalIdeal R].TFAE
• CategoryTheory.Abelian.tfae_epi 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) (Z : C) : [CategoryTheory.Epi f, CategoryTheory.Limits.cokernel.π f = 0, { X₁ := X, X₂ := Y, X₃ := Z, f := f, g := 0, zero := ⋯ }.Exact].TFAE
• CategoryTheory.Abelian.tfae_mono 📋 Mathlib.CategoryTheory.Abelian.Exact
  {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Abelian C] {X Y : C} (f : X ⟶ Y) (Z : C) : [CategoryTheory.Mono f, CategoryTheory.Limits.kernel.ι f = 0, { X₁ := Z, X₂ := X, X₃ := Y, f := 0, g := f, zero := ⋯ }.Exact].TFAE
• CategoryTheory.Functor.exact_tfae 📋 Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).ShortExact, ∀ (S : CategoryTheory.ShortComplex C), S.Exact → (S.map F).Exact, F.PreservesHomology, CategoryTheory.Limits.PreservesFiniteLimits F ∧ CategoryTheory.Limits.PreservesFiniteColimits F].TFAE
• CategoryTheory.Functor.preservesFiniteColimits_tfae 📋 Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g), ∀ (S : CategoryTheory.ShortComplex C), S.Exact ∧ CategoryTheory.Epi S.g → (S.map F).Exact ∧ CategoryTheory.Epi (F.map S.g), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f 0) F, CategoryTheory.Limits.PreservesFiniteColimits F].TFAE
• CategoryTheory.Functor.preservesFiniteLimits_tfae 📋 Mathlib.Algebra.Homology.ShortComplex.ExactFunctor
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.Abelian C] [CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [F.Additive] : [∀ (S : CategoryTheory.ShortComplex C), S.ShortExact → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f), ∀ (S : CategoryTheory.ShortComplex C), S.Exact ∧ CategoryTheory.Mono S.f → (S.map F).Exact ∧ CategoryTheory.Mono (F.map S.f), ∀ ⦃X Y : C⦄ (f : X ⟶ Y), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F, CategoryTheory.Limits.PreservesFiniteLimits F].TFAE
• AddCommGroup.tfae_modEq 📋 Mathlib.Algebra.Order.ToIntervalMod
  {α : Type u_1} [AddCommGroup α] [LinearOrder α] [IsOrderedAddMonoid α] [hα : Archimedean α] {p : α} (hp : 0 < p) (a b : α) : [a ≡ b [PMOD p], ∀ (z : ℤ), b - z • p ∉ Set.Ioo a (a + p), toIcoMod hp a b ≠ toIocMod hp a b, toIcoMod hp a b + p = toIocMod hp a b].TFAE
• specializes_TFAE 📋 Mathlib.Topology.Inseparable
  {X : Type u_1} [TopologicalSpace X] (x y : X) : [x ⤳ y, pure x ≤ nhds y, ∀ (s : Set X), IsOpen s → y ∈ s → x ∈ s, ∀ (s : Set X), IsClosed s → x ∈ s → y ∈ s, y ∈ closure {x}, closure {y} ⊆ closure {x}, ClusterPt y (pure x)].TFAE
• t1Space_TFAE 📋 Mathlib.Topology.Separation.Basic
  (X : Type u) [TopologicalSpace X] : [T1Space X, ∀ (x : X), IsClosed {x}, ∀ (x : X), IsOpen {x}ᶜ, Continuous ⇑CofiniteTopology.of, ∀ ⦃x y : X⦄, x ≠ y → {y}ᶜ ∈ nhds x, ∀ ⦃x y : X⦄, x ≠ y → ∃ s ∈ nhds x, y ∉ s, ∀ ⦃x y : X⦄, x ≠ y → ∃ U, IsOpen U ∧ x ∈ U ∧ y ∉ U, ∀ ⦃x y : X⦄, x ≠ y → Disjoint (nhds x) (pure y), ∀ ⦃x y : X⦄, x ≠ y → Disjoint (pure x) (nhds y), ∀ ⦃x y : X⦄, x ⤳ y → x = y, T0Space X ∧ R0Space X].TFAE
• regularSpace_TFAE 📋 Mathlib.Topology.Separation.Regular
  (X : Type u) [TopologicalSpace X] : [RegularSpace X, ∀ (s : Set X), ∀ x ∉ closure s, Disjoint (nhdsSet s) (nhds x), ∀ (x : X) (s : Set X), Disjoint (nhdsSet s) (nhds x) ↔ x ∉ closure s, ∀ (x : X), ∀ s ∈ nhds x, ∃ t ∈ nhds x, IsClosed t ∧ t ⊆ s, ∀ (x : X), (nhds x).lift' closure ≤ nhds x, ∀ (x : X), (nhds x).lift' closure = nhds x].TFAE
• tendstoLocallyUniformlyOn_TFAE 📋 Mathlib.Topology.UniformSpace.LocallyUniformConvergence
  {α : Type u_1} {β : Type u_2} {ι : Type u_4} [TopologicalSpace α] [UniformSpace β] {s : Set α} [LocallyCompactSpace α] (G : ι → α → β) (g : α → β) (p : Filter ι) (hs : IsOpen s) : [TendstoLocallyUniformlyOn G g p s, ∀ K ⊆ s, IsCompact K → TendstoUniformlyOn G g p K, ∀ x ∈ s, ∃ v ∈ nhdsWithin x s, TendstoUniformlyOn G g p v].TFAE
• TFAE_mem_nhdsGE 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a b : α} (hab : a < b) (s : Set α) : [s ∈ nhdsWithin a (Set.Ici a), s ∈ nhdsWithin a (Set.Icc a b), s ∈ nhdsWithin a (Set.Ico a b), ∃ u ∈ Set.Ioc a b, Set.Ico a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ico a u ⊆ s].TFAE
• TFAE_mem_nhdsGT 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a b : α} (hab : a < b) (s : Set α) : [s ∈ nhdsWithin a (Set.Ioi a), s ∈ nhdsWithin a (Set.Ioc a b), s ∈ nhdsWithin a (Set.Ioo a b), ∃ u ∈ Set.Ioc a b, Set.Ioo a u ⊆ s, ∃ u ∈ Set.Ioi a, Set.Ioo a u ⊆ s].TFAE
• TFAE_mem_nhdsLE 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a b : α} (h : a < b) (s : Set α) : [s ∈ nhdsWithin b (Set.Iic b), s ∈ nhdsWithin b (Set.Icc a b), s ∈ nhdsWithin b (Set.Ioc a b), ∃ l ∈ Set.Ico a b, Set.Ioc l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioc l b ⊆ s].TFAE
• TFAE_mem_nhdsLT 📋 Mathlib.Topology.Order.LeftRightNhds
  {α : Type u_1} [TopologicalSpace α] [LinearOrder α] [OrderTopology α] {a b : α} (h : a < b) (s : Set α) : [s ∈ nhdsWithin b (Set.Iio b), s ∈ nhdsWithin b (Set.Ico a b), s ∈ nhdsWithin b (Set.Ioo a b), ∃ l ∈ Set.Ico a b, Set.Ioo l b ⊆ s, ∃ l ∈ Set.Iio b, Set.Ioo l b ⊆ s].TFAE
• isLocallyClosed_tfae 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] (s : Set X) : [IsLocallyClosed s, ∀ x ∈ s, IsLocallyClosedAt s x, ∀ x ∈ coborder s, IsLocallyClosedAt s x, IsOpen (coborder s), ∃ U, IsOpen U ∧ s = U ∩ closure s, IsOpen (Subtype.val ⁻¹' s)].TFAE
• isLocallyClosedAt_tfae 📋 Mathlib.Topology.LocallyClosed
  {X : Type u_1} [TopologicalSpace X] (s : Set X) (x : X) : [IsLocallyClosedAt s x, ∃ U ∈ nhds x, IsClosed (Subtype.val ⁻¹' s), ∃ U ∈ nhds x, U ∩ closure s ⊆ s, ∃ U ∈ nhds x, U ∩ s = U ∩ closure s, ∃ Z, IsClosed Z ∧ s =ᶠ[nhds x] Z, s =ᶠ[nhds x] closure s, closure s ≤ᶠ[nhds x] s, s ∈ nhdsWithin x (closure s), coborder s ∈ nhds x].TFAE
• TopologicalSpace.noetherianSpace_TFAE 📋 Mathlib.Topology.NoetherianSpace
  (α : Type u_1) [TopologicalSpace α] : [TopologicalSpace.NoetherianSpace α, WellFoundedLT (TopologicalSpace.Closeds α), ∀ (s : Set α), IsCompact s, ∀ (s : TopologicalSpace.Opens α), IsCompact ↑s].TFAE
• IsSemisimpleModule.finite_tfae 📋 Mathlib.RingTheory.FiniteLength
  {R : Type u_1} [Ring R] {M : Type u_2} [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] : [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M, ∃ s, s.Finite ∧ sSupIndep s ∧ sSup s = ⊤ ∧ ∀ m ∈ s, IsSimpleModule R ↥m].TFAE
• Valuation.isEquiv_tfae 📋 Mathlib.RingTheory.Valuation.Basic
  {K : Type u_1} [DivisionRing K] {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [LinearOrderedCommGroupWithZero Γ₀] [LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation K Γ₀) (v' : Valuation K Γ'₀) : [v.IsEquiv v', ∀ {x y : K}, v x < v y ↔ v' x < v' y, ∀ {x : K}, v x ≤ 1 ↔ v' x ≤ 1, ∀ {x : K}, v x = 1 ↔ v' x = 1, ∀ {x : K}, v x < 1 ↔ v' x < 1, ∀ {x : K}, v (x - 1) < 1 ↔ v' (x - 1) < 1].TFAE
• IsBezout.TFAE 📋 Mathlib.RingTheory.Bezout
  {R : Type u} [CommRing R] [IsBezout R] [IsDomain R] : [IsNoetherianRing R, IsPrincipalIdealRing R, UniqueFactorizationMonoid R, WfDvdMonoid R].TFAE
• ValuationRing.TFAE 📋 Mathlib.RingTheory.Valuation.ValuationRing
  (R : Type u) [CommRing R] [IsDomain R] : [ValuationRing R, ∀ (x : FractionRing R), IsLocalization.IsInteger R x ∨ IsLocalization.IsInteger R x⁻¹, Std.Total fun x1 x2 => x1 ∣ x2, Std.Total fun x1 x2 => x1 ≤ x2, IsLocalRing R ∧ IsBezout R].TFAE
• Ring.krullDimLE_zero_and_isLocalRing_tfae 📋 Mathlib.RingTheory.KrullDimension.Zero
  (R : Type u_1) [CommSemiring R] : [Ring.KrullDimLE 0 R ∧ IsLocalRing R, ∃! I, I.IsPrime, ∀ (x : R), IsNilpotent x ↔ ¬IsUnit x, (nilradical R).IsMaximal].TFAE
• IsDiscreteValuationRing.TFAE 📋 Mathlib.RingTheory.DiscreteValuationRing.TFAE
  (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] (h : ¬IsField R) : [IsDiscreteValuationRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∃! P, P ≠ ⊥ ∧ P.IsPrime, Submodule.IsPrincipal (IsLocalRing.maximalIdeal R), Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) = 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = IsLocalRing.maximalIdeal R ^ n].TFAE
• tfae_of_isNoetherianRing_of_isLocalRing_of_isDomain 📋 Mathlib.RingTheory.DiscreteValuationRing.TFAE
  (R : Type u_1) [CommRing R] [IsNoetherianRing R] [IsLocalRing R] [IsDomain R] : [IsPrincipalIdealRing R, ValuationRing R, IsDedekindDomain R, IsIntegrallyClosed R ∧ ∀ (P : Ideal R), P ≠ ⊥ → P.IsPrime → P = IsLocalRing.maximalIdeal R, Submodule.IsPrincipal (IsLocalRing.maximalIdeal R), Module.finrank (IsLocalRing.ResidueField R) (IsLocalRing.CotangentSpace R) ≤ 1, ∀ (I : Ideal R), I ≠ ⊥ → ∃ n, I = IsLocalRing.maximalIdeal R ^ n].TFAE
• LinearMap.charpoly_nilpotent_tfae 📋 Mathlib.LinearAlgebra.Eigenspace.Zero
  {R : Type u_1} {M : Type u_3} [CommRing R] [IsDomain R] [AddCommGroup M] [Module R M] [Module.Finite R M] [Module.Free R M] [IsNoetherian R M] (φ : Module.End R M) : [IsNilpotent φ, LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M, ∀ (m : M), ∃ n, (φ ^ n) m = 0, (LinearMap.charpoly φ).natTrailingDegree = Module.finrank R M].TFAE
• LinearMap.not_hasEigenvalue_zero_tfae 📋 Mathlib.LinearAlgebra.Eigenspace.Zero
  {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] (φ : Module.End K M) : [¬φ.HasEigenvalue 0, ¬(minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) ≠ 0, LinearMap.det φ ≠ 0, LinearMap.ker φ = ⊥, ∀ (m : M), φ m = 0 → m = 0].TFAE
• LinearMap.hasEigenvalue_zero_tfae 📋 Mathlib.LinearAlgebra.Eigenspace.Zero
  {K : Type u_2} {M : Type u_3} [Field K] [AddCommGroup M] [Module K M] [Module.Finite K M] (φ : Module.End K M) : [φ.HasEigenvalue 0, (minpoly K φ).IsRoot 0, Polynomial.constantCoeff (LinearMap.charpoly φ) = 0, LinearMap.det φ = 0, ⊥ < LinearMap.ker φ, ∃ m, m ≠ 0 ∧ φ m = 0].TFAE
• Module.Flat.tfae_equational_criterion 📋 Mathlib.RingTheory.Flat.EquationalCriterion
  (R : Type u_1) (M : Type u_2) [CommRing R] [AddCommGroup M] [Module R M] : [Module.Flat R M, ∀ (I : Ideal R), Function.Injective ⇑(LinearMap.rTensor M (Submodule.subtype I)), ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i ⊗ₜ[R] x i = 0 → TensorProduct.VanishesTrivially R f x, ∀ {l : ℕ} {f : Fin l → R} {x : Fin l → M}, ∑ i, f i • x i = 0 → Module.IsTrivialRelation f x, ∀ {l : ℕ} {f : Fin l →₀ R} {x : (Fin l →₀ R) →ₗ[R] M}, x f = 0 → ∃ k a y, x = y ∘ₗ a ∧ a f = 0].TFAE
• IsLocallyConstant.tfae 📋 Mathlib.Topology.LocallyConstant.Basic
  {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] (f : X → Y) : [IsLocallyConstant f, ∀ (x : X), ∀ᶠ (x' : X) in nhds x, f x' = f x, ∀ (x : X), IsOpen {x' | f x' = f x}, ∀ (y : Y), IsOpen (f ⁻¹' {y}), ∀ (x : X), ∃ U, IsOpen U ∧ x ∈ U ∧ ∀ x' ∈ U, f x' = f x].TFAE
• IsArtinianRing.tfae 📋 Mathlib.RingTheory.HopkinsLevitzki
  (R : Type u_2) (M : Type u) [Ring R] [AddCommGroup M] [Module R M] [IsArtinianRing R] : [Module.Finite R M, IsNoetherian R M, IsArtinian R M, IsFiniteLength R M].TFAE
• PrimeSpectrum.isOpen_singleton_tfae_of_isNoetherian_of_isJacobsonRing 📋 Mathlib.RingTheory.Spectrum.Prime.Jacobson
  {R : Type u_1} [CommRing R] [IsNoetherianRing R] [IsJacobsonRing R] (x : PrimeSpectrum R) : [IsOpen {x}, IsClopen {x}, IsClosed {x} ∧ StableUnderGeneralization {x}].TFAE
• Matroid.isLoop_tfae 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (e : α) : [M.IsLoop e, e ∈ M.closure ∅, M.IsCircuit {e}, M.Dep {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ M.E \ B].TFAE
• Matroid.isColoop_tfae 📋 Mathlib.Combinatorics.Matroid.Loop
  {α : Type u_1} (M : Matroid α) (e : α) : [M.IsColoop e, e ∈ M.coloops, M.IsCocircuit {e}, ∀ ⦃B : Set α⦄, M.IsBase B → e ∈ B, (∀ ⦃C : Set α⦄, M.IsCircuit C → e ∉ C) ∧ e ∈ M.E, ∀ (X : Set α), e ∈ M.closure X ↔ e ∈ X, ¬M.Spanning (M.E \ {e})].TFAE
• IsGalois.tfae 📋 Mathlib.FieldTheory.Galois.Basic
  {F : Type u_1} [Field F] {E : Type u_2} [Field E] [Algebra F E] [FiniteDimensional F E] : [IsGalois F E, IntermediateField.fixedField ⊤ = ⊥, Nat.card Gal(E/F) = Module.finrank F E, ∃ p, p.Separable ∧ Polynomial.IsSplittingField F E p].TFAE
• MeasureTheory.Measure.mutuallySingular_tfae 📋 Mathlib.MeasureTheory.Measure.MutuallySingular
  {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} : [μ.MutuallySingular ν, Disjoint μ ν, Disjoint (MeasureTheory.ae μ) (MeasureTheory.ae ν)].TFAE
• MeasureTheory.smulInvariantMeasure_tfae 📋 Mathlib.MeasureTheory.Group.Action
  (G : Type u) {α : Type w} {m : MeasurableSpace α} [Group G] [MulAction G α] (μ : MeasureTheory.Measure α) [MeasurableConstSMul G α] : [MeasureTheory.SMulInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c • s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x => c • x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c • s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun x => c • x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c • x) μ μ].TFAE
• MeasureTheory.vaddInvariantMeasure_tfae 📋 Mathlib.MeasureTheory.Group.Action
  (G : Type u) {α : Type w} {m : MeasurableSpace α} [AddGroup G] [AddAction G α] (μ : MeasureTheory.Measure α) [MeasurableConstVAdd G α] : [MeasureTheory.VAddInvariantMeasure G α μ, ∀ (c : G) (s : Set α), MeasurableSet s → μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), MeasurableSet s → μ (c +ᵥ s) = μ s, ∀ (c : G) (s : Set α), μ ((fun x => c +ᵥ x) ⁻¹' s) = μ s, ∀ (c : G) (s : Set α), μ (c +ᵥ s) = μ s, ∀ (c : G), MeasureTheory.Measure.map (fun x => c +ᵥ x) μ = μ, ∀ (c : G), MeasureTheory.MeasurePreserving (fun x => c +ᵥ x) μ μ].TFAE
• RCLike.is_real_TFAE 📋 Mathlib.Analysis.RCLike.Basic
  {K : Type u_1} [RCLike K] (z : K) : [(starRingEnd K) z = z, ∃ r, ↑r = z, ↑(RCLike.re z) = z, RCLike.im z = 0, IsSelfAdjoint z].TFAE
• TFAE_exists_lt_isLittleO_pow 📋 Mathlib.Analysis.SpecificLimits.Normed
  (f : ℕ → ℝ) (R : ℝ) : [∃ a ∈ Set.Ioo (-R) R, f =o[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =o[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo (-R) R, f =O[Filter.atTop] fun x => a ^ x, ∃ a ∈ Set.Ioo 0 R, f =O[Filter.atTop] fun x => a ^ x, ∃ a < R, ∃ C, (0 < C ∨ 0 < R) ∧ ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a ∈ Set.Ioo 0 R, ∃ C > 0, ∀ (n : ℕ), |f n| ≤ C * a ^ n, ∃ a < R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n, ∃ a ∈ Set.Ioo 0 R, ∀ᶠ (n : ℕ) in Filter.atTop, |f n| ≤ a ^ n].TFAE
• WithSeminorms.equicontinuous_TFAE 📋 Mathlib.Analysis.LocallyConvex.WithSeminorms
  {𝕜 : Type u_2} {𝕜₂ : Type u_3} {E : Type u_6} {F : Type u_7} {ι' : Type u_10} [NontriviallyNormedField 𝕜] [AddCommGroup E] [Module 𝕜 E] [NormedField 𝕜₂] [AddCommGroup F] [Module 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] {κ : Type u_11} {q : SeminormFamily 𝕜₂ F ι'} [UniformSpace E] [IsUniformAddGroup E] [u : UniformSpace F] [hu : IsUniformAddGroup F] (hq : WithSeminorms q) [ContinuousSMul 𝕜 E] (f : κ → E →ₛₗ[σ₁₂] F) : [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), ∀ (i : ι'), ∃ p, Continuous ⇑p ∧ ∀ (k : κ), (q i).comp (f k) ≤ p, ∀ (i : ι'), BddAbove (Set.range fun k => (q i).comp (f k)) ∧ Continuous (⨆ k, ⇑((q i).comp (f k)))].TFAE
• NormedSpace.equicontinuous_TFAE 📋 Mathlib.Analysis.Normed.Operator.NormedSpace
  {𝕜 : Type u_1} {𝕜₂ : Type u_3} {E : Type u_5} {F : Type u_6} {ι : Type u_9} [NontriviallyNormedField 𝕜] [NontriviallyNormedField 𝕜₂] {σ₁₂ : 𝕜 →+* 𝕜₂} [RingHomIsometric σ₁₂] [SeminormedAddCommGroup E] [SeminormedAddCommGroup F] [NormedSpace 𝕜 E] [NormedSpace 𝕜₂ F] (f : ι → E →SL[σ₁₂] F) : [EquicontinuousAt (DFunLike.coe ∘ f) 0, Equicontinuous (DFunLike.coe ∘ f), UniformEquicontinuous (DFunLike.coe ∘ f), ∃ C, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C ≥ 0, ∀ (i : ι) (x : E), ‖(f i) x‖ ≤ C * ‖x‖, ∃ C, ∀ (i : ι), ‖f i‖ ≤ C, ∃ C ≥ 0, ∀ (i : ι), ‖f i‖ ≤ C, BddAbove (Set.range fun x => ‖f x‖), ⨆ i, ↑‖f i‖₊ < ⊤].TFAE
• norm_inner_eq_norm_tfae 📋 Mathlib.Analysis.InnerProductSpace.Basic
  (𝕜 : Type u_1) {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (x y : E) : [‖inner 𝕜 x y‖ = ‖x‖ * ‖y‖, x = 0 ∨ y = (inner 𝕜 x y / inner 𝕜 x x) • x, x = 0 ∨ ∃ r, y = r • x, x = 0 ∨ y ∈ 𝕜 ∙ x].TFAE
• BoxIntegral.Box.le_TFAE 📋 Mathlib.Analysis.BoxIntegral.Box.Basic
  {ι : Type u_1} (I J : BoxIntegral.Box ι) : [I ≤ J, ↑I ⊆ ↑J, Set.Icc I.lower I.upper ⊆ Set.Icc J.lower J.upper, J.lower ≤ I.lower ∧ I.upper ≤ J.upper].TFAE
• AlgebraicGeometry.tfae_universallyInjective 📋 Mathlib.AlgebraicGeometry.Morphisms.UniversallyInjective
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) : [AlgebraicGeometry.UniversallyInjective f, ∀ (K : Type u) [inst : Field K], Function.Injective fun g => CategoryTheory.CategoryStruct.comp g f, Function.Injective ⇑f ∧ ∀ (x : ↥X), (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.residueFieldMap f x)).IsPurelyInseparable, AlgebraicGeometry.Surjective (CategoryTheory.Limits.pullback.diagonal f)].TFAE
• traceForm_nondegenerate_tfae 📋 Mathlib.RingTheory.Trace.Basic
  (K : Type u_3) (L : Type u_4) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] : [Algebra.IsSeparable K L, Algebra.trace K L ≠ 0, (Algebra.traceForm K L).Nondegenerate].TFAE
• Module.Flat.tfae_algebraMap_surjective 📋 Mathlib.RingTheory.Flat.Rank
  (R : Type u_1) (S : Type u_2) [CommRing R] [CommRing S] [Algebra R S] [Module.Flat R S] [Module.Finite R S] : [Function.Surjective ⇑(algebraMap R S), Function.Bijective ⇑(LinearMap.mul' R S), ∀ (p : PrimeSpectrum R), Module.rankAtStalk S p ≤ 1].TFAE
• CStarAlgebra.nonneg_TFAE 📋 Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
  {A : Type u_1} [PartialOrder A] [NonUnitalRing A] [TopologicalSpace A] [StarRing A] [Module ℝ A] [SMulCommClass ℝ A A] [IsScalarTower ℝ A A] [StarOrderedRing A] [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A} : [0 ≤ a, a = CFC.sqrt a * CFC.sqrt a, ∃ b, 0 ≤ b ∧ a = b * b, ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b, ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0, IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE
• CStarAlgebra.isStrictlyPositive_TFAE 📋 Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
  {A : Type u_1} [PartialOrder A] [Ring A] [StarRing A] [TopologicalSpace A] [StarOrderedRing A] [Algebra ℝ A] [ContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A} : [IsStrictlyPositive a, IsStrictlyPositive (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a, IsUnit (CFC.sqrt a) ∧ a = CFC.sqrt a * CFC.sqrt a, ∃ b, IsStrictlyPositive b ∧ a = b * b, ∃ b, IsUnit b ∧ IsSelfAdjoint b ∧ a = b * b, ∃ b, IsUnit b ∧ a = star b * b, ∃ b, IsUnit b ∧ a = b * star b, 0 ≤ a ∧ IsUnit a, IsSelfAdjoint a ∧ ∀ x ∈ spectrum ℝ a, 0 < x].TFAE
• IsStarProjection.le_tfae 📋 Mathlib.Analysis.CStarAlgebra.Projection
  {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {p q : A} (hp : IsStarProjection p) (hq : IsStarProjection q) : [p ≤ q, q * p = p, p * q = p, IsStarProjection (q - p), IsIdempotentElem (q - p)].TFAE
• ConcaveOn.continuousOn_tfae 📋 Mathlib.Analysis.Convex.Continuous
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} (hC : IsOpen C) (hC' : C.Nonempty) (hf : ConcaveOn ℝ C f) : [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀, ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (nhds x₀) f, ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) (nhds x₀) f, ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) |f|].TFAE
• ConvexOn.continuousOn_tfae 📋 Mathlib.Analysis.Convex.Continuous
  {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {C : Set E} {f : E → ℝ} (hC : IsOpen C) (hC' : C.Nonempty) (hf : ConvexOn ℝ C f) : [LocallyLipschitzOn C f, ContinuousOn f C, ∃ x₀ ∈ C, ContinuousAt f x₀, ∃ x₀ ∈ C, Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) f, ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) f, ∀ ⦃x₀ : E⦄, x₀ ∈ C → Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) (nhds x₀) |f|].TFAE
• ContinuousLinearMap.IsIdempotentElem.TFAE 📋 Mathlib.Analysis.InnerProductSpace.Positive
  {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] {p : E →L[𝕜] E} (hp : IsIdempotentElem p) : [(↑p).rangeᗮ = (↑p).ker, IsStarNormal p, IsSelfAdjoint p, p.IsPositive].TFAE
• LinearMap.normDet_ne_zero_tfae 📋 Mathlib.Analysis.InnerProductSpace.NormDet
  {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) : [f.normDet ≠ 0, f.ker = ⊥, Module.finrank 𝕜 ↥f.range = Module.finrank 𝕜 U, Nonempty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 ↥f.range), Function.Injective ⇑f].TFAE
• LinearMap.normDet_eq_zero_tfae 📋 Mathlib.Analysis.InnerProductSpace.NormDet
  {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [RCLike 𝕜] [NormedAddCommGroup U] [InnerProductSpace 𝕜 U] [FiniteDimensional 𝕜 U] [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] (f : U →ₗ[𝕜] V) : [f.normDet = 0, f.ker ≠ ⊥, Module.finrank 𝕜 ↥f.range ≠ Module.finrank 𝕜 U, Module.finrank 𝕜 ↥f.range < Module.finrank 𝕜 U, IsEmpty (OrthonormalBasis (Fin (Module.finrank 𝕜 U)) 𝕜 ↥f.range), ¬Function.Injective ⇑f].TFAE
• RKHS.posSemidef_tfae 📋 Mathlib.Analysis.InnerProductSpace.Reproducing
  {𝕜 : Type u_1} [RCLike 𝕜] {X : Type u_2} {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace 𝕜 V] [CompleteSpace V] {K : Matrix X X (V →L[𝕜] V)} : [K.PosSemidef, K.IsHermitian ∧ ∀ (f : X × V →₀ 𝕜), 0 ≤ RCLike.re (f.sum fun xv z => f.sum fun xv' w => (starRingEnd 𝕜) z * w * inner 𝕜 ((K xv'.1 xv.1) xv.2) xv'.2), K.IsHermitian ∧ ∀ (vv : X →₀ V), 0 ≤ RCLike.re (vv.sum fun x w => vv.sum fun x' w' => inner 𝕜 ((K x' x) w) w')].TFAE
• ContinuousLinearMap.isFredholm_tfae 📋 Mathlib.Analysis.Normed.Operator.Fredholm.Basic
  {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [AddCommGroup E] [AddCommGroup F] [Module 𝕜 E] [Module 𝕜 F] [TopologicalSpace E] [TopologicalSpace F] [CompleteSpace 𝕜] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] [T2Space E] [T2Space F] (u : E →L[𝕜] F) : [u.IsFredholm, ∃ v, (↑v).IsQuasiInverse ↑u, ∃ E₁ F₁, IsClosed ↑E₁ ∧ IsClosed ↑F₁ ∧ E₁.CoFG ∧ F₁.CoFG ∧ ∃ (h : Set.MapsTo ⇑u ↑E₁ ↑F₁), (u.restrict h).IsInvertible, Nonempty u.FredholmPackage].TFAE
• CategoryTheory.ObjectProperty.SerreClassLocalization.epi_map_tfae 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : [CategoryTheory.Epi (L.map f), P.epiModSerre f, ∀ ⦃Z : C⦄ (z : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (L.map f) (L.map z) = 0 → L.map z = 0].TFAE
• CategoryTheory.ObjectProperty.SerreClassLocalization.mono_map_tfae 📋 Mathlib.CategoryTheory.Abelian.SerreClass.Localization
  {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C) [P.IsSerreClass] [L.IsLocalization P.isoModSerre] [CategoryTheory.Preadditive D] [L.Additive] {X Y : C} (f : X ⟶ Y) : [CategoryTheory.Mono (L.map f), P.monoModSerre f, ∀ ⦃Z : C⦄ (z : Z ⟶ X), CategoryTheory.CategoryStruct.comp (L.map z) (L.map f) = 0 → L.map z = 0].TFAE
• CategoryTheory.Bicategory.isLeftAdjoint_TFAE 📋 Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (f : a ⟶ b) : [CategoryTheory.Bicategory.IsLeftAdjoint f, CategoryTheory.Bicategory.HasAbsLeftKanExtension f (CategoryTheory.CategoryStruct.id a), ∃ (x : CategoryTheory.Bicategory.HasLeftKanExtension f (CategoryTheory.CategoryStruct.id a)), CategoryTheory.Bicategory.Lan.CommuteWith f (CategoryTheory.CategoryStruct.id a) f].TFAE
• CategoryTheory.Bicategory.isRightAdjoint_TFAE 📋 Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
  {B : Type u} [CategoryTheory.Bicategory B] {a b : B} (u : b ⟶ a) : [CategoryTheory.Bicategory.IsRightAdjoint u, CategoryTheory.Bicategory.HasAbsLeftKanLift u (CategoryTheory.CategoryStruct.id a), ∃ (x : CategoryTheory.Bicategory.HasLeftKanLift u (CategoryTheory.CategoryStruct.id a)), CategoryTheory.Bicategory.LanLift.CommuteWith u (CategoryTheory.CategoryStruct.id a) u].TFAE
• CategoryTheory.Monoidal.Reflective.isIso_tfae 📋 Mathlib.CategoryTheory.Monoidal.Braided.Reflection
  {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Category.{v_2, u_2} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.SymmetricCategory D] [CategoryTheory.MonoidalClosed D] {R : CategoryTheory.Functor C D} [R.Faithful] [R.Full] {L : CategoryTheory.Functor D C} (adj : L ⊣ R) : [∀ (c : C) (d : D), CategoryTheory.IsIso (adj.unit.app (d ⟹ R.obj c)), ∀ (c : C) (d : D), CategoryTheory.IsIso ((CategoryTheory.MonoidalClosed.pre (adj.unit.app d)).app (R.obj c)), ∀ (d d' : D), CategoryTheory.IsIso (L.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight (adj.unit.app d) d')), ∀ (d d' : D), CategoryTheory.IsIso (L.map (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app d) (adj.unit.app d')))].TFAE
• Cardinal.SharplyLT.tfae 📋 Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
  {κ₁ κ₂ : Cardinal.{w}} [Fact κ₁.IsRegular] [Fact κ₂.IsRegular] (h : κ₁ < κ₂) : [κ₁.SharplyLT κ₂, CategoryTheory.IsCardinalAccessibleCategory (CategoryTheory.CardinalDirectedPoset κ₁) κ₂, ∀ (C : Type (w + 1)) [inst : CategoryTheory.Category.{w, w + 1} C] [CategoryTheory.IsCardinalAccessibleCategory C κ₁], CategoryTheory.IsCardinalAccessibleCategory C κ₂, ∀ (X : Type w), HasCardinalLT X κ₂ → ∃ A, HasCardinalLT (↑A) κ₂ ∧ IsCofinal A, ∀ ⦃X : Type w⦄ [inst : PartialOrder X] [CategoryTheory.IsCardinalFiltered X κ₁] (A : Set X), HasCardinalLT (↑A) κ₂ → ∃ B, A ⊆ B ∧ CategoryTheory.IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂].TFAE
• Graph.IsClosedSubgraph.mem_tfae_of_isLink 📋 Mathlib.Combinatorics.Graph.Subgraph
  {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β} (he : G.IsLink e x y) (hHG : H.IsClosedSubgraph G) : [x ∈ H.vertexSet, y ∈ H.vertexSet, e ∈ H.edgeSet].TFAE
• CompHaus.effectiveEpi_tfae 📋 Mathlib.Topology.Category.CompHaus.EffectiveEpi
  {B X : CompHaus} (π : X ⟶ B) : [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
• CompHaus.effectiveEpiFamily_tfae 📋 Mathlib.Topology.Category.CompHaus.EffectiveEpi
  {α : Type} [Finite α] {B : CompHaus} (X : α → CompHaus) (π : (a : α) → X a ⟶ B) : [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
• Profinite.effectiveEpi_tfae 📋 Mathlib.Topology.Category.Profinite.EffectiveEpi
  {B X : Profinite} (π : X ⟶ B) : [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
• Profinite.effectiveEpiFamily_tfae 📋 Mathlib.Topology.Category.Profinite.EffectiveEpi
  {α : Type} [Finite α] {B : Profinite} (X : α → Profinite) (π : (a : α) → X a ⟶ B) : [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
• Stonean.effectiveEpi_tfae 📋 Mathlib.Topology.Category.Stonean.EffectiveEpi
  {B X : Stonean} (π : X ⟶ B) : [CategoryTheory.EffectiveEpi π, CategoryTheory.Epi π, Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom π)].TFAE
• Stonean.effectiveEpiFamily_tfae 📋 Mathlib.Topology.Category.Stonean.EffectiveEpi
  {α : Type} [Finite α] {B : Stonean} (X : α → Stonean) (π : (a : α) → X a ⟶ B) : [CategoryTheory.EffectiveEpiFamily X π, CategoryTheory.Epi (CategoryTheory.Limits.Sigma.desc π), ∀ (b : ↑B.toTop), ∃ a x, (CategoryTheory.ConcreteCategory.hom (π a)) x = b].TFAE
• LightCondSet.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (X : LightCondSet) : [LightCondensed.IsDiscrete X, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (Type u)).counit.app X), (LightCondensed.discrete (Type u)).essImage X, LightCondSet.LocallyConstant.functor.essImage X, CategoryTheory.IsIso (LightCondSet.LocallyConstant.adjunction.counit.app X), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (X.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE
• LightCondMod.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (R : Type u) [Ring R] (M : LightCondMod R) : [LightCondensed.IsDiscrete M, CategoryTheory.IsIso ((LightCondensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), (LightCondensed.discrete (ModuleCat R)).essImage M, (LightCondMod.LocallyConstant.functor R).essImage M, CategoryTheory.IsIso ((LightCondMod.LocallyConstant.adjunction R).counit.app M), ∀ (S : LightProfinite), Nonempty (CategoryTheory.Limits.IsColimit (M.obj.mapCocone (CategoryTheory.Limits.coconeRightOpOfCone S.asLimitCone)))].TFAE
• CondensedSet.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (X : CondensedSet) : [Condensed.IsDiscrete X, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (Type (u + 1))).counit.app X), (Condensed.discrete (Type (u + 1))).essImage X, CondensedSet.LocallyConstant.functor.essImage X, CategoryTheory.IsIso (CondensedSet.LocallyConstant.adjunction.counit.app X), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).inverse.obj X), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp X.obj).mapCocone S.asLimitCone.op))].TFAE
• CondensedMod.isDiscrete_tfae 📋 Mathlib.Condensed.Discrete.Characterization
  (R : Type (u + 1)) [Ring R] (M : CondensedMod R) : [Condensed.IsDiscrete M, CategoryTheory.IsIso ((Condensed.discreteUnderlyingAdj (ModuleCat R)).counit.app M), (Condensed.discrete (ModuleCat R)).essImage M, (CondensedMod.LocallyConstant.functor R).essImage M, CategoryTheory.IsIso ((CondensedMod.LocallyConstant.adjunction R).counit.app M), CategoryTheory.Sheaf.IsConstant (CategoryTheory.coherentTopology Profinite) ((Condensed.ProfiniteCompHaus.equivalence (ModuleCat R)).inverse.obj M), ∀ (S : Profinite), Nonempty (CategoryTheory.Limits.IsColimit ((profiniteToCompHaus.op.comp M.obj).mapCocone S.asLimitCone.op))].TFAE
• isCyclic_tfae 📋 Mathlib.FieldTheory.KummerExtension
  (K : Type u_1) (L : Type u_2) [Field K] [Field L] [Algebra K L] [FiniteDimensional K L] (hK : (primitiveRoots (Module.finrank K L) K).Nonempty) : [IsGalois K L ∧ IsCyclic Gal(L/K), ∃ a, Irreducible (Polynomial.X ^ Module.finrank K L - Polynomial.C a) ∧ Polynomial.IsSplittingField K L (Polynomial.X ^ Module.finrank K L - Polynomial.C a), ∃ α, α ^ Module.finrank K L ∈ Set.range ⇑(algebraMap K L) ∧ K⟮α⟯ = ⊤].TFAE
• isNilpotent_of_finite_tfae 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [hG : Group G] [Finite G] : [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal, ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal, Nonempty (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE
• Group.isNilpotent_of_finite_tfae 📋 Mathlib.GroupTheory.Nilpotent
  {G : Type u_1} [hG : Group G] [Finite G] : [Group.IsNilpotent G, NormalizerCondition G, ∀ (H : Subgroup G), IsCoatom H → H.Normal, ∀ (p : ℕ), Fact (Nat.Prime p) → ∀ (P : Sylow p G), (↑P).Normal, Nonempty (((p : ↥(Nat.card G).primeFactors) → (P : Sylow (↑p) G) → ↥↑P) ≃* G)].TFAE
• fermatLastTheoremWith'_nat_int_tfae 📋 Mathlib.NumberTheory.FLT.Basic
  (n : ℕ) : [FermatLastTheoremFor n, FermatLastTheoremWith' ℕ n, FermatLastTheoremWith' ℤ n].TFAE
• fermatLastTheoremWith_nat_int_rat_tfae 📋 Mathlib.NumberTheory.FLT.Basic
  (n : ℕ) : [FermatLastTheoremWith ℕ n, FermatLastTheoremWith ℤ n, FermatLastTheoremWith ℚ n].TFAE
• ModuleCat.exists_isRegular_tfae 📋 Mathlib.RingTheory.Depth.Rees
  {R : Type u} [CommRing R] [Small.{v, u} R] [IsNoetherianRing R] (I : Ideal R) (n : ℕ) (M : ModuleCat R) [Module.Finite R ↑M] (smul_lt : I • ⊤ < ⊤) : [∀ (N : ModuleCat R), Nontrivial ↑N → Module.Finite R ↑N → Module.support R ↑N ⊆ PrimeSpectrum.zeroLocus ↑I → ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i), ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext (ModuleCat.of R (Shrink.{v, u} (R ⧸ I))) M i), ∃ N, Nontrivial ↑N ∧ Module.Finite R ↑N ∧ Module.support R ↑N = PrimeSpectrum.zeroLocus ↑I ∧ ∀ i < n, Subsingleton (CategoryTheory.Abelian.Ext N M i), ∃ rs, rs.length = n ∧ (∀ r ∈ rs, r ∈ I) ∧ RingTheory.Sequence.IsRegular (↑M) rs].TFAE
• HenselianLocalRing.TFAE 📋 Mathlib.RingTheory.Henselian
  (R : Type u) [CommRing R] [IsLocalRing R] : [HenselianLocalRing R, ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : IsLocalRing.ResidueField R), (Polynomial.aeval a₀) f = 0 → (Polynomial.aeval a₀) (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ (IsLocalRing.residue R) a = a₀, ∀ {K : Type u} [inst : Field K] (φ : R →+* K), Function.Surjective ⇑φ → ∀ (f : Polynomial R), f.Monic → ∀ (a₀ : K), Polynomial.eval₂ φ a₀ f = 0 → Polynomial.eval₂ φ a₀ (Polynomial.derivative f) ≠ 0 → ∃ a, f.IsRoot a ∧ φ a = a₀].TFAE
• IsLocalRing.not_isLocalRing_tfae 📋 Mathlib.RingTheory.LocalRing.NonLocalRing
  {R : Type u_1} [CommSemiring R] [Nontrivial R] : [¬IsLocalRing R, Nontrivial (MaximalSpectrum R), ∃ m₁ m₂, m₁.IsMaximal ∧ m₂.IsMaximal ∧ m₁ ≠ m₂].TFAE
• IsSimpleRing.tfae 📋 Mathlib.RingTheory.SimpleModule.WedderburnArtin
  {R : Type u} [Ring R] [IsSimpleRing R] : [IsSemisimpleRing R, IsArtinianRing R, ∃ I, IsAtom I].TFAE
• Ordinal.mem_closure_tfae 📋 Mathlib.SetTheory.Ordinal.Topology
  (a : Ordinal.{u}) (s : Set Ordinal.{u}) : [a ∈ closure s, a ∈ closure (s ∩ Set.Iic a), (s ∩ Set.Iic a).Nonempty ∧ sSup (s ∩ Set.Iic a) = a, ∃ t ⊆ s, t.Nonempty ∧ BddAbove t ∧ sSup t = a, ∃ ι, Nonempty ι ∧ ∃ f, (∀ (i : ι), f i ∈ s) ∧ ⨆ i, f i = a].TFAE
• mapClusterPt_atTop_nsmul_tfae 📋 Mathlib.Topology.Algebra.Group.SubmonoidClosure
  {G : Type u_1} [AddGroup G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G] (x y : G) : [MapClusterPt x Filter.atTop fun x => x • y, MapClusterPt x Filter.atTop fun x => x • y, x ∈ closure (Set.range fun x => x • y), x ∈ closure (Set.range fun x => x • y)].TFAE
• mapClusterPt_atTop_pow_tfae 📋 Mathlib.Topology.Algebra.Group.SubmonoidClosure
  {G : Type u_1} [Group G] [TopologicalSpace G] [CompactSpace G] [IsTopologicalGroup G] (x y : G) : [MapClusterPt x Filter.atTop fun x => y ^ x, MapClusterPt x Filter.atTop fun x => y ^ x, x ∈ closure (Set.range fun x => y ^ x), x ∈ closure (Set.range fun x => y ^ x)].TFAE

About

Loogle searches Lean and Mathlib definitions and theorems.

You can use Loogle from within the Lean4 VSCode language extension using the Loogle command from the command palette. 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.

5. You can filter for definitions vs theorems: Using ⊢ (_ : Type _) finds all definitions which provide data while ⊢ (_ : Prop) finds all theorems (and definitions of proofs).

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, _ * _, _ ^ _, |- _ < _ → _
would 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. Please review the Lean FRO Terms of Use and Privacy Policy.

This is Loogle revision 9f11169 serving mathlib revision 69fae59