Loogle!

Result

Found 118 declarations mentioning Projectivization.

Projectivization 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Type u_2
Projectivization.rep 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : V
Projectivization.instNonemptyOfNontrivial 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] [Nontrivial V] : Nonempty (Projectivization K V)
Projectivization.submodule 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : Submodule K V
Projectivization.submodule_injective 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] : Function.Injective Projectivization.submodule
Projectivization.mk 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : V) (hv : v ≠ 0) : Projectivization K V
Projectivization.mk' 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : { v // v ≠ 0 }) : Projectivization K V
Projectivization.rep_nonzero 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : v.rep ≠ 0
Projectivization.mk''_submodule 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : Projectivization.mk'' v.submodule ⋯ = v
Projectivization.mk_rep 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : Projectivization.mk K v.rep ⋯ = v
Projectivization.ind 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {P : Projectivization K V → Prop} (h : ∀ (v : V) (h : v ≠ 0), P (Projectivization.mk K v h)) (p : Projectivization K V) : P p
Projectivization.submodule_eq 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : v.submodule = K ∙ v.rep
Projectivization.mk.congr_simp 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v v✝ : V) (e_v : v = v✝) (hv : v ≠ 0) : Projectivization.mk K v hv = Projectivization.mk K v✝ ⋯
Projectivization.mk'_eq_mk 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : { v // v ≠ 0 }) : Projectivization.mk' K v = Projectivization.mk K ↑v ⋯
Projectivization.instFiniteDimensionalSubtypeMemSubmoduleSubmodule 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : FiniteDimensional K ↥v.submodule
Projectivization.mk'' 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (H : Submodule K V) (h : Module.finrank K ↥H = 1) : Projectivization K V
Projectivization.finrank_submodule 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v : Projectivization K V) : Module.finrank K ↥v.submodule = 1
Projectivization.equivSubmodule 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) (V : Type u_2) [DivisionRing K] [AddCommGroup V] [Module K V] : Projectivization K V ≃ { H // Module.finrank K ↥H = 1 }
Projectivization.map_id 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] : Projectivization.map LinearMap.id ⋯ = id
Projectivization.map 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) : Projectivization K V → Projectivization L W
Projectivization.mk_eq_mk_iff' 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : Projectivization.mk K v hv = Projectivization.mk K w hw ↔ ∃ a, a • w = v
Projectivization.map_injective 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} {τ : L →+* K} [RingHomInvPair σ τ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) : Function.Injective (Projectivization.map f hf)
Projectivization.mk_eq_mk_iff 📋 Mathlib.LinearAlgebra.Projectivization.Basic
(K : Type u_1) {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) : Projectivization.mk K v hv = Projectivization.mk K w hw ↔ ∃ a, a • w = v
Projectivization.lift 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {α : Type u_3} (f : { v // v ≠ 0 } → α) (hf : ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b) (x : Projectivization K V) : α
Projectivization.map.congr_simp 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} (f f✝ : V →ₛₗ[σ] W) (e_f : f = f✝) (hf : Function.Injective ⇑f) (a✝ a✝¹ : Projectivization K V) : a✝ = a✝¹ → Projectivization.map f hf a✝ = Projectivization.map f✝ ⋯ a✝¹
Projectivization.map_comp 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {F : Type u_5} {U : Type u_6} [DivisionRing F] [AddCommGroup U] [Module F U] {σ : K →+* L} {τ : L →+* F} {γ : K →+* F} [RingHomCompTriple σ τ γ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) (g : W →ₛₗ[τ] U) (hg : Function.Injective ⇑g) (hgf : Function.Injective ⇑(g ∘ₛₗ f) := ⋯) : Projectivization.map (g ∘ₛₗ f) hgf = Projectivization.map g hg ∘ Projectivization.map f hf
Projectivization.map_mk 📋 Mathlib.LinearAlgebra.Projectivization.Basic
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {L : Type u_3} {W : Type u_4} [DivisionRing L] [AddCommGroup W] [Module L W] {σ : K →+* L} (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) (v : V) (hv : v ≠ 0) : Projectivization.map f hf (Projectivization.mk K v hv) = Projectivization.mk L (f v) ⋯
Projectivization.orthogonal 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] {m : Type u_2} [Fintype m] : Projectivization F (m → F) → Projectivization F (m → F) → Prop
Projectivization.orthogonal_comm 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] {m : Type u_2} [Fintype m] {v w : Projectivization F (m → F)} : v.orthogonal w ↔ w.orthogonal v
Projectivization.cross_self 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] (v : Projectivization F (Fin 3 → F)) : v.cross v = v
Projectivization.exists_not_orthogonal_self 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] {m : Type u_2} [Fintype m] (v : Projectivization F (m → F)) : ∃ w, ¬w.orthogonal v
Projectivization.exists_not_self_orthogonal 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] {m : Type u_2} [Fintype m] (v : Projectivization F (m → F)) : ∃ w, ¬v.orthogonal w
Projectivization.cross 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] : Projectivization F (Fin 3 → F) → Projectivization F (Fin 3 → F) → Projectivization F (Fin 3 → F)
Projectivization.cross_comm 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] (v w : Projectivization F (Fin 3 → F)) : v.cross w = w.cross v
Projectivization.cross_orthogonal_left 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] {v w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : (v.cross w).orthogonal v
Projectivization.cross_orthogonal_right 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] {v w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : (v.cross w).orthogonal w
Projectivization.orthogonal_cross_left 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] {v w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : v.orthogonal (v.cross w)
Projectivization.orthogonal_cross_right 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] {v w : Projectivization F (Fin 3 → F)} (h : v ≠ w) : w.orthogonal (v.cross w)
Projectivization.mk_eq_mk_iff_crossProduct_eq_zero 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) : Projectivization.mk F v hv = Projectivization.mk F w hw ↔ (crossProduct v) w = 0
Projectivization.cross_mk_of_cross_eq_zero 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : (crossProduct v) w = 0) : (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F v hv
Projectivization.cross_mk_of_cross_ne_zero 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : (crossProduct v) w ≠ 0) : (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F ((crossProduct v) w) h
Projectivization.cross_mk_of_ne 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) (h : Projectivization.mk F v hv ≠ Projectivization.mk F w hw) : (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = Projectivization.mk F ((crossProduct v) w) ⋯
Projectivization.cross_mk 📋 Mathlib.LinearAlgebra.Projectivization.Constructions
{F : Type u_1} [Field F] [DecidableEq F] {v w : Fin 3 → F} (hv : v ≠ 0) (hw : w ≠ 0) : (Projectivization.mk F v hv).cross (Projectivization.mk F w hw) = if h : (crossProduct v) w = 0 then Projectivization.mk F v hv else Projectivization.mk F ((crossProduct v) w) h
Configuration.ofField.instMembershipProjectivizationForallFinOfNatNat 📋 Mathlib.Combinatorics.Configuration
{K : Type u_3} [Field K] : Membership (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))
Configuration.ofField.instNondegenerateProjectivizationForallFinOfNatNat 📋 Mathlib.Combinatorics.Configuration
{K : Type u_3} [Field K] : Configuration.Nondegenerate (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))
Configuration.ofField.instProjectivePlaneProjectivizationForallFinOfNatNatOfDecidableEq 📋 Mathlib.Combinatorics.Configuration
{K : Type u_3} [Field K] [DecidableEq K] : Configuration.ProjectivePlane (Projectivization K (Fin 3 → K)) (Projectivization K (Fin 3 → K))
Configuration.ofField.mem_iff 📋 Mathlib.Combinatorics.Configuration
{K : Type u_3} [Field K] (v w : Projectivization K (Fin 3 → K)) : v ∈ w ↔ v.orthogonal w
Configuration.ofField.eq_or_eq_of_orthogonal 📋 Mathlib.Combinatorics.Configuration
{K : Type u_3} [Field K] {a b c d : Projectivization K (Fin 3 → K)} (hac : a.orthogonal c) (hbc : b.orthogonal c) (had : a.orthogonal d) (hbd : b.orthogonal d) : a = b ∨ c = d
Projectivization.instMulAction 📋 Mathlib.LinearAlgebra.Projectivization.Action
{G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] [Group G] [DistribMulAction G V] [SMulCommClass G K V] : MulAction G (Projectivization K V)
Projectivization.smul_mk 📋 Mathlib.LinearAlgebra.Projectivization.Action
{G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] [Group G] [DistribMulAction G V] [SMulCommClass G K V] (g : G) {v : V} (hv : v ≠ 0) : g • Projectivization.mk K v hv = Projectivization.mk K (g • v) ⋯
Projectivization.smul_def 📋 Mathlib.LinearAlgebra.Projectivization.Action
{G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] [Group G] [DistribMulAction G V] [SMulCommClass G K V] (g : G) (x : Projectivization K V) : SMul.smul g x = Projectivization.map ((DistribMulAction.toModuleEnd K V) g) ⋯ x
Projectivization.generalLinearGroup_smul_def 📋 Mathlib.LinearAlgebra.Projectivization.Action
{K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] (g : LinearMap.GeneralLinearGroup K V) (x : Projectivization K V) : g • x = Projectivization.map ↑g.toLinearEquiv ⋯ x
Projectivization.finite_of_finite 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] [Finite V] : Finite (Projectivization k V)
Projectivization.isEmpty_of_subsingleton 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] [Subsingleton V] : IsEmpty (Projectivization k V)
Projectivization.finite_iff_of_finite 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] [Finite k] : Finite (Projectivization k V) ↔ Finite V
Projectivization.nonZeroEquivProjectivizationProdUnits 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] : { v // v ≠ 0 } ≃ Projectivization k V × kˣ
Projectivization.card 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] : Nat.card V - 1 = Nat.card (Projectivization k V) * (Nat.card k - 1)
Projectivization.card' 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] [Finite V] : Nat.card V = Nat.card (Projectivization k V) * (Nat.card k - 1) + 1
Projectivization.card'' 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Finite k] : Nat.card (Projectivization k V) = (Nat.card V - 1) / (Nat.card k - 1)
Projectivization.card_of_finrank_two 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Finite k] (h : Module.finrank k V = 2) : Nat.card (Projectivization k V) = Nat.card k + 1
Projectivization.card_of_finrank 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [Field k] [AddCommGroup V] [Module k V] [Finite k] {n : ℕ} (h : Module.finrank k V = n) : Nat.card (Projectivization k V) = ∑ i ∈ Finset.range n, Nat.card k ^ i
Projectivization.equivQuotientOrbitRel 📋 Mathlib.LinearAlgebra.Projectivization.Cardinality
(k : Type u_1) (V : Type u_2) [DivisionRing k] [AddCommGroup V] [Module k V] : Projectivization k V ≃ Quotient (MulAction.orbitRel kˣ { v // v ≠ 0 })
Projectivization.Dependent 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] : (ι → Projectivization K V) → Prop
Projectivization.Independent 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] : (ι → Projectivization K V) → Prop
Projectivization.dependent_iff_not_independent 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {f : ι → Projectivization K V} : Projectivization.Dependent f ↔ ¬Projectivization.Independent f
Projectivization.independent_iff_not_dependent 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {f : ι → Projectivization K V} : Projectivization.Independent f ↔ ¬Projectivization.Dependent f
Projectivization.independent_iff 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {f : ι → Projectivization K V} : Projectivization.Independent f ↔ LinearIndependent K (Projectivization.rep ∘ f)
Projectivization.dependent_iff 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {f : ι → Projectivization K V} : Projectivization.Dependent f ↔ ¬LinearIndependent K (Projectivization.rep ∘ f)
Projectivization.independent_iff_iSupIndep 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{ι : Type u_1} {K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] {f : ι → Projectivization K V} : Projectivization.Independent f ↔ iSupIndep fun i => (f i).submodule
Projectivization.dependent_pair_iff_eq 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] (u v : Projectivization K V) : Projectivization.Dependent ![u, v] ↔ u = v
Projectivization.independent_pair_iff_ne 📋 Mathlib.LinearAlgebra.Projectivization.Independence
{K : Type u_2} {V : Type u_3} [DivisionRing K] [AddCommGroup V] [Module K V] (u v : Projectivization K V) : Projectivization.Independent ![u, v] ↔ u ≠ v
Projectivization.Subspace.carrier 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (self : Projectivization.Subspace K V) : Set (Projectivization K V)
Projectivization.Subspace.instSetLike 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : SetLike (Projectivization.Subspace K V) (Projectivization K V)
Projectivization.Subspace.span 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) : Projectivization.Subspace K V
Projectivization.Subspace.spanCarrier 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) : Set (Projectivization K V)
Projectivization.Subspace.span_coe 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (W : Projectivization.Subspace K V) : Projectivization.Subspace.span ↑W = W
Projectivization.Subspace.spanCarrier.below 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {motive : (a : Projectivization K V) → Projectivization.Subspace.spanCarrier S a → Prop} {a✝ : Projectivization K V} (t : Projectivization.Subspace.spanCarrier S a✝) : Prop
Projectivization.Subspace.ext 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} {inst✝ : Field K} {inst✝¹ : AddCommGroup V} {inst✝² : Module K V} {x y : Projectivization.Subspace K V} (carrier : x.carrier = y.carrier) : x = y
Projectivization.Subspace.ext_iff 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} {inst✝ : Field K} {inst✝¹ : AddCommGroup V} {inst✝² : Module K V} {x y : Projectivization.Subspace K V} : x = y ↔ x.carrier = y.carrier
Projectivization.Subspace.spanCarrier.of 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} (x : Projectivization K V) (hx : x ∈ S) : Projectivization.Subspace.spanCarrier S x
Projectivization.Subspace.subset_span 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (S : Set (Projectivization K V)) : S ⊆ ↑(Projectivization.Subspace.span S)
Projectivization.Subspace.span_iUnion 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {ι : Sort u_3} (s : ι → Set (Projectivization K V)) : Projectivization.Subspace.span (⋃ i, s i) = ⨆ i, Projectivization.Subspace.span (s i)
Projectivization.Subspace.spanCarrier.brecOn 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {motive : (a : Projectivization K V) → Projectivization.Subspace.spanCarrier S a → Prop} {a✝ : Projectivization K V} (t : Projectivization.Subspace.spanCarrier S a✝) (F_1 : ∀ (a : Projectivization K V) (t : Projectivization.Subspace.spanCarrier S a), Projectivization.Subspace.spanCarrier.below t → motive a t) : motive a✝ t
Projectivization.Subspace.spanCarrier.below.of 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {motive : (a : Projectivization K V) → Projectivization.Subspace.spanCarrier S a → Prop} (x : Projectivization K V) (hx : x ∈ S) : Projectivization.Subspace.spanCarrier.below ⋯
Projectivization.Subspace.mem_carrier_iff 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (A : Projectivization.Subspace K V) (x : Projectivization K V) : x ∈ A.carrier ↔ x ∈ A
Projectivization.Subspace.span_eq_sInf 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} : Projectivization.Subspace.span S = sInf {W | S ⊆ ↑W}
Projectivization.Subspace.span_le_span 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {s t : Set (Projectivization K V)} (hst : s ⊆ t) : Projectivization.Subspace.span s ≤ Projectivization.Subspace.span t
Projectivization.Subspace.span_le_subspace_iff 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V} : Projectivization.Subspace.span S ≤ W ↔ S ⊆ ↑W
Projectivization.Subspace.span_union 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (S T : Set (Projectivization K V)) : Projectivization.Subspace.span (S ∪ T) = Projectivization.Subspace.span S ⊔ Projectivization.Subspace.span T
Projectivization.Subspace.monotone_span 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Monotone Projectivization.Subspace.span
Projectivization.Subspace.span_sup 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V} : Projectivization.Subspace.span S ⊔ W = Projectivization.Subspace.span (S ∪ ↑W)
Projectivization.Subspace.sup_span 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V} : W ⊔ Projectivization.Subspace.span S = Projectivization.Subspace.span (↑W ∪ S)
Projectivization.Subspace.span_eq_of_le 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {W : Projectivization.Subspace K V} (hS : S ⊆ ↑W) (hW : W ≤ Projectivization.Subspace.span S) : Projectivization.Subspace.span S = W
Projectivization.Subspace.gi 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : GaloisInsertion Projectivization.Subspace.span SetLike.coe
Projectivization.Subspace.span_eq_span_iff 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S T : Set (Projectivization K V)} : Projectivization.Subspace.span S = Projectivization.Subspace.span T ↔ S ⊆ ↑(Projectivization.Subspace.span T) ∧ T ⊆ ↑(Projectivization.Subspace.span S)
Projectivization.Subspace.span_univ 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Projectivization.Subspace.span Set.univ = ⊤
Projectivization.Subspace.mem_span 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} (u : Projectivization K V) : u ∈ Projectivization.Subspace.span S ↔ ∀ (W : Projectivization.Subspace K V), S ⊆ ↑W → u ∈ W
Projectivization.Subspace.span_empty 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] : Projectivization.Subspace.span ∅ = ⊥
Projectivization.Subspace.spanCarrier.mem_add 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0) : Projectivization.Subspace.spanCarrier S (Projectivization.mk K v hv) → Projectivization.Subspace.spanCarrier S (Projectivization.mk K w hw) → Projectivization.Subspace.spanCarrier S (Projectivization.mk K (v + w) hvw)
Projectivization.Subspace.subset_span_trans 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S T U : Set (Projectivization K V)} (hST : S ⊆ ↑(Projectivization.Subspace.span T)) (hTU : T ⊆ ↑(Projectivization.Subspace.span U)) : S ⊆ ↑(Projectivization.Subspace.span U)
Projectivization.Subspace.mk 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (carrier : Set (Projectivization K V)) (mem_add' : ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), Projectivization.mk K v hv ∈ carrier → Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier) : Projectivization.Subspace K V
Projectivization.Subspace.mem_add' 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (self : Projectivization.Subspace K V) (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0) : Projectivization.mk K v hv ∈ self.carrier → Projectivization.mk K w hw ∈ self.carrier → Projectivization.mk K (v + w) hvw ∈ self.carrier
Projectivization.Subspace.mem_add 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (T : Projectivization.Subspace K V) (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0) : Projectivization.mk K v hv ∈ T → Projectivization.mk K w hw ∈ T → Projectivization.mk K (v + w) hvw ∈ T
Projectivization.Subspace.spanCarrier.below.mem_add 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] {S : Set (Projectivization K V)} {motive : (a : Projectivization K V) → Projectivization.Subspace.spanCarrier S a → Prop} (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0) (a✝ : Projectivization.Subspace.spanCarrier S (Projectivization.mk K v hv)) (a✝¹ : Projectivization.Subspace.spanCarrier S (Projectivization.mk K w hw)) : Projectivization.Subspace.spanCarrier.below a✝ → motive (Projectivization.mk K v hv) a✝ → Projectivization.Subspace.spanCarrier.below a✝¹ → motive (Projectivization.mk K w hw) a✝¹ → Projectivization.Subspace.spanCarrier.below ⋯
Projectivization.Subspace.mk.sizeOf_spec 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [SizeOf K] [SizeOf V] (carrier : Set (Projectivization K V)) (mem_add' : ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), Projectivization.mk K v hv ∈ carrier → Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier) : sizeOf { carrier := carrier, mem_add' := mem_add' } = 1
Projectivization.Subspace.mem_submodule_iff 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (s : Projectivization.Subspace K V) {v : V} (hv : v ≠ 0) : v ∈ Projectivization.Subspace.submodule s ↔ Projectivization.mk K v hv ∈ s
Submodule.mk_mem_projectivization_iff 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (s : Submodule K V) {v : V} (hv : v ≠ 0) : Projectivization.mk K v hv ∈ Submodule.projectivization s ↔ v ∈ s
Submodule.mem_projectivization_iff_submodule_le 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (s : Submodule K V) (x : Projectivization K V) : x ∈ Submodule.projectivization s ↔ x.submodule ≤ s
Projectivization.Subspace.mk.injEq 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (carrier : Set (Projectivization K V)) (mem_add' : ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), Projectivization.mk K v hv ∈ carrier → Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier) (carrier✝ : Set (Projectivization K V)) (mem_add'✝ : ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), Projectivization.mk K v hv ∈ carrier✝ → Projectivization.mk K w hw ∈ carrier✝ → Projectivization.mk K (v + w) hvw ∈ carrier✝) : ({ carrier := carrier, mem_add' := mem_add' } = { carrier := carrier✝, mem_add' := mem_add'✝ }) = (carrier = carrier✝)
Projectivization.Subspace.mk.congr_simp 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] (carrier carrier✝ : Set (Projectivization K V)) (e_carrier : carrier = carrier✝) (mem_add' : ∀ (v w : V) (hv : v ≠ 0) (hw : w ≠ 0) (hvw : v + w ≠ 0), Projectivization.mk K v hv ∈ carrier → Projectivization.mk K w hw ∈ carrier → Projectivization.mk K (v + w) hvw ∈ carrier) : { carrier := carrier, mem_add' := mem_add' } = { carrier := carrier✝, mem_add' := ⋯ }
Projectivization.lift.congr_simp 📋 Mathlib.LinearAlgebra.Projectivization.Subspace
{K : Type u_1} {V : Type u_2} [DivisionRing K] [AddCommGroup V] [Module K V] {α : Type u_3} (f f✝ : { v // v ≠ 0 } → α) (e_f : f = f✝) (hf : ∀ (a b : { v // v ≠ 0 }) (t : K), ↑a = t • ↑b → f a = f b) (x x✝ : Projectivization K V) (e_x : x = x✝) : Projectivization.lift f hf x = Projectivization.lift f✝ ⋯ x✝
OnePoint.equivProjectivization 📋 Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
(K : Type u_1) [DivisionRing K] [DecidableEq K] : OnePoint K ≃ Projectivization K (K × K)
Projectivization.instMulAction.congr_simp 📋 Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
{G : Type u_1} {K : Type u_2} {V : Type u_3} [AddCommGroup V] [DivisionRing K] [Module K V] [Group G] [DistribMulAction G V] [SMulCommClass G K V] : Projectivization.instMulAction = Projectivization.instMulAction
OnePoint.equivProjectivization_apply_coe 📋 Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
(K : Type u_1) [DivisionRing K] [DecidableEq K] (t : K) : (OnePoint.equivProjectivization K) ↑t = Projectivization.mk K (t, 1) ⋯
OnePoint.equivProjectivization_apply_infinity 📋 Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
(K : Type u_1) [DivisionRing K] [DecidableEq K] : (OnePoint.equivProjectivization K) OnePoint.infty = Projectivization.mk K (1, 0) ⋯
OnePoint.equivProjectivization_symm_apply_mk 📋 Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
(K : Type u_1) [DivisionRing K] [DecidableEq K] (x y : K) (h : (x, y) ≠ 0) : (OnePoint.equivProjectivization K).symm (Projectivization.mk K (x, y) h) = if y = 0 then OnePoint.infty else ↑(y⁻¹ * x)
OnePoint.equivProjectivization.eq_1 📋 Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
(K : Type u_1) [DivisionRing K] [DecidableEq K] : OnePoint.equivProjectivization K = { toFun := fun p => p.elim (Projectivization.mk K (1, 0) ⋯) fun t => Projectivization.mk K (t, 1) ⋯, invFun := fun p => Projectivization.lift (fun u => if (↑u).2 = 0 then OnePoint.infty else ↑((↑u).2⁻¹ * (↑u).1)) ⋯ p, left_inv := ⋯, right_inv := ⋯ }
OnePoint.smul_infty_def 📋 Mathlib.Topology.Compactification.OnePoint.ProjectiveLine
{K : Type u_1} [Field K] [DecidableEq K] {g : GL (Fin 2) K} : g • OnePoint.infty = (OnePoint.equivProjectivization K).symm (Projectivization.mk K (↑g 0 0, ↑g 1 0) ⋯)

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

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 find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

If you pass more than one such search filter, separated by commas Loogle will return lemmas which match all of them. The search
🔍 Real.sin, "two", tsum, _ * _, _ ^ _, |- _ < _ → _
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.

This is Loogle revision 6ff4759 serving mathlib revision 1047f07