Loogle!

Result

Found 11 declarations mentioning Matrix and Module.Finite.

• Module.Finite.matrix 📋 Mathlib.LinearAlgebra.FreeModule.Finite.Basic
  {R : Type u_1} {ι₁ : Type u_2} {ι₂ : Type u_3} {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] [Module.Free R M] [Module.Finite R M] [Finite ι₁] [Finite ι₂] : Module.Finite R (Matrix ι₁ ι₂ M)
• LinearMap.charpoly.eq_1 📋 Mathlib.LinearAlgebra.Charpoly.Basic
  {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) : f.charpoly = ((LinearMap.toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M)) f).charpoly
• LinearMap.charpoly_def 📋 Mathlib.LinearAlgebra.Charpoly.Basic
  {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) : f.charpoly = ((LinearMap.toMatrix (Module.Free.chooseBasis R M) (Module.Free.chooseBasis R M)) f).charpoly
• Matrix.charpoly_toLin 📋 Mathlib.LinearAlgebra.Charpoly.ToMatrix
  {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] {n : Type u_5} [Fintype n] [DecidableEq n] (A : Matrix n n R) (b : Module.Basis n R M) : ((Matrix.toLin b b) A).charpoly = A.charpoly
• LinearMap.charpoly_toMatrix 📋 Mathlib.LinearAlgebra.Charpoly.ToMatrix
  {R : Type u_1} {M : Type u_2} [CommRing R] [AddCommGroup M] [Module R M] [Module.Free R M] [Module.Finite R M] (f : M →ₗ[R] M) {ι : Type w} [DecidableEq ι] [Fintype ι] (b : Module.Basis ι R M) : ((LinearMap.toMatrix b b) f).charpoly = f.charpoly
• Algebra.traceMatrix_eq_embeddingsMatrixReindex_mul_trans 📋 Mathlib.RingTheory.Trace.Basic
  (K : Type u_4) {L : Type u_5} [Field K] [Field L] [Algebra K L] {κ : Type w} (E : Type z) [Field E] [Algebra K E] [Module.Finite K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (b : κ → L) [Fintype κ] (e : κ ≃ (L →ₐ[K] E)) : (Algebra.traceMatrix K b).map ⇑(algebraMap K E) = Algebra.embeddingsMatrixReindex K E b e * (Algebra.embeddingsMatrixReindex K E b e).transpose
• Algebra.traceMatrix_eq_embeddingsMatrix_mul_trans 📋 Mathlib.RingTheory.Trace.Basic
  (K : Type u_4) {L : Type u_5} [Field K] [Field L] [Algebra K L] {κ : Type w} (E : Type z) [Field E] [Algebra K E] [Module.Finite K L] [Algebra.IsSeparable K L] [IsAlgClosed E] (b : κ → L) : (Algebra.traceMatrix K b).map ⇑(algebraMap K E) = Algebra.embeddingsMatrix K E b * (Algebra.embeddingsMatrix K E b).transpose
• IsSimpleRing.exists_algEquiv_matrix_divisionRing_finite 📋 Mathlib.RingTheory.SimpleModule.WedderburnArtin
  (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSimpleRing R] [IsArtinianRing R] [Module.Finite R₀ R] : ∃ n, ∃ (_ : NeZero n), ∃ D x x_1, ∃ (_ : Module.Finite R₀ D), Nonempty (R ≃ₐ[R₀] Matrix (Fin n) (Fin n) D)
• IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite 📋 Mathlib.RingTheory.SimpleModule.WedderburnArtin
  (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] [IsSemisimpleRing R] [Module.Finite R₀ R] : ∃ n D d x x_1, ∃ (_ : ∀ (i : Fin n), Module.Finite R₀ (D i)), (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (R ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (D i))
• IsSemisimpleModule.exists_end_ringEquiv 📋 Mathlib.RingTheory.SimpleModule.WedderburnArtin
  (R : Type u) [Ring R] (M : Type u_2) [AddCommGroup M] [Module R M] [IsSemisimpleModule R M] [Module.Finite R M] : ∃ n S d, (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧ (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃+* ((i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i))))
• IsSemisimpleModule.exists_end_algEquiv 📋 Mathlib.RingTheory.SimpleModule.WedderburnArtin
  (R₀ : Type u_1) (R : Type u) [CommSemiring R₀] [Ring R] [Algebra R₀ R] (M : Type u_2) [AddCommGroup M] [Module R₀ M] [Module R M] [IsScalarTower R₀ R M] [IsSemisimpleModule R M] [Module.Finite R M] : ∃ n S d, (∀ (i : Fin n), IsSimpleModule R ↥(S i)) ∧ (∀ (i : Fin n), NeZero (d i)) ∧ Nonempty (Module.End R M ≃ₐ[R₀] (i : Fin n) → Matrix (Fin (d i)) (Fin (d i)) (Module.End R ↥(S i)))

About

Loogle searches Lean and Mathlib definitions and theorems.

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

Usage

Loogle finds definitions and lemmas in various ways:

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

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

3. By subexpression:
   🔍 _ * (_ ^ _)
   finds all lemmas whose statements somewhere include a product where the second argument is raised to some power.

   The pattern can also be non-linear, as in
   🔍 Real.sqrt ?a * Real.sqrt ?a

   If the pattern has parameters, they are matched in any order. Both of these will find List.map:
   🔍 (?a -> ?b) -> List ?a -> List ?b
   🔍 List ?a -> (?a -> ?b) -> List ?b

4. By main conclusion:
   🔍 |- tsum _ = _ * tsum _
   finds all lemmas where the conclusion (the subexpression to the right of all → and ∀) has the given shape.

   As before, if the pattern has parameters, they are matched against the hypotheses of the lemma in any order; for example,
   🔍 |- _ < _ → tsum _ < tsum _
   will find tsum_lt_tsum even though the hypothesis f i < g i is not the last.

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