Loogle!
Result
Found 127 declarations mentioning Matrix.map.
- Matrix.map 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (M : Matrix m n α) (f : α → β) : Matrix m n β - Matrix.map_id 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : M.map id = M - Matrix.map_id' 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} (M : Matrix m n α) : (M.map fun x => x) = M - Matrix.map_apply 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {f : α → β} {i : m} {j : n} : M.map f i j = f (M i j) - Matrix.map_injective 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} (hf : Function.Injective f) : Function.Injective fun M => M.map f - Matrix.col_map 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (A : Matrix m n α) (f : α → β) (j : n) : (A.map f).col j = f ∘ A.col j - Matrix.row_map 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (A : Matrix m n α) (f : α → β) (i : m) : (A.map f).row i = f ∘ A.row i - Matrix.transpose_map 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {M : Matrix m n α} : M.transpose.map f = (M.map f).transpose - Matrix.map_map 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {β : Type u_10} {γ : Type u_11} {f : α → β} {g : β → γ} : (M.map f).map g = M.map (g ∘ f) - Matrix.submatrix_map 📋 Mathlib.Data.Matrix.Defs
{l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} (f : α → β) (e₁ : l → m) (e₂ : o → n) (A : Matrix m n α) : (A.map f).submatrix e₁ e₂ = (A.submatrix e₁ e₂).map f - Matrix.map_zero 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Zero α] [Zero β] (f : α → β) (h : f 0 = 0) : Matrix.map 0 f = 0 - Matrix.map_smul 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [SMul R α] [SMul R β] (f : α → β) (r : R) (hf : ∀ (a : α), f (r • a) = r • f a) (M : Matrix m n α) : (r • M).map f = r • M.map f - Matrix.map_smul' 📋 Mathlib.Data.Matrix.Defs
{n : Type u_3} {α : Type v} {β : Type w} [Mul α] [Mul β] (f : α → β) (r : α) (A : Matrix n n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) : (r • A).map f = f r • A.map f - Matrix.map_add 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Add α] [Add β] (f : α → β) (hf : ∀ (a₁ a₂ : α), f (a₁ + a₂) = f a₁ + f a₂) (M N : Matrix m n α) : (M + N).map f = M.map f + N.map f - Matrix.map_sub 📋 Mathlib.Data.Matrix.Defs
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Sub α] [Sub β] (f : α → β) (hf : ∀ (a₁ a₂ : α), f (a₁ - a₂) = f a₁ - f a₂) (M N : Matrix m n α) : (M - N).map f = M.map f - N.map f - Matrix.map_op_smul' 📋 Mathlib.Data.Matrix.Defs
{n : Type u_3} {α : Type v} {β : Type w} [Mul α] [Mul β] (f : α → β) (r : α) (A : Matrix n n α) (hf : ∀ (a₁ a₂ : α), f (a₁ * a₂) = f a₁ * f a₂) : (MulOpposite.op r • A).map f = MulOpposite.op (f r) • A.map f - Matrix.diag_map 📋 Mathlib.Data.Matrix.Diagonal
{n : Type u_3} {α : Type v} {β : Type w} {f : α → β} {A : Matrix n n α} : (A.map f).diag = f ∘ A.diag - Matrix.diagonal_map 📋 Mathlib.Data.Matrix.Diagonal
{n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [Zero α] [Zero β] {f : α → β} (h : f 0 = 0) {d : n → α} : (Matrix.diagonal d).map f = Matrix.diagonal fun m => f (d m) - Matrix.map_natCast 📋 Mathlib.Data.Matrix.Diagonal
{n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddMonoidWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℕ) : (↑d).map f = Matrix.diagonal fun x => f ↑d - Matrix.map_intCast 📋 Mathlib.Data.Matrix.Diagonal
{n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddGroupWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℤ) : (↑d).map f = Matrix.diagonal fun x => f ↑d - Matrix.map_one 📋 Mathlib.Data.Matrix.Diagonal
{n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [Zero α] [One α] [Zero β] [One β] (f : α → β) (h₀ : f 0 = 0) (h₁ : f 1 = 1) : Matrix.map 1 f = 1 - Matrix.map_ofNat 📋 Mathlib.Data.Matrix.Diagonal
{n : Type u_3} {α : Type v} {β : Type w} [DecidableEq n] [AddMonoidWithOne α] [Zero β] {f : α → β} (h : f 0 = 0) (d : ℕ) [d.AtLeastTwo] : (OfNat.ofNat d).map f = Matrix.diagonal fun x => f (OfNat.ofNat d) - RingHom.map_mulVec 📋 Mathlib.Data.Matrix.Mul
{m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix m n R) (v : n → R) (i : m) : f (M.mulVec v i) = (M.map ⇑f).mulVec (⇑f ∘ v) i - RingHom.map_vecMul 📋 Mathlib.Data.Matrix.Mul
{m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} [Fintype n] [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (M : Matrix n m R) (v : n → R) (i : m) : f (Matrix.vecMul v M i) = Matrix.vecMul (⇑f ∘ v) (M.map ⇑f) i - RingHom.map_matrix_mul 📋 Mathlib.Data.Matrix.Mul
{m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [Fintype n] [NonAssocSemiring α] [NonAssocSemiring β] (M : Matrix m n α) (N : Matrix n o α) (i : m) (j : o) (f : α →+* β) : f ((M * N) i j) = (M.map ⇑f * N.map ⇑f) i j - Matrix.map_mul 📋 Mathlib.Data.Matrix.Mul
{m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} {β : Type w} [NonAssocSemiring α] [Fintype n] {L : Matrix m n α} {M : Matrix n o α} [NonAssocSemiring β] {f : α →+* β} : (L * M).map ⇑f = L.map ⇑f * M.map ⇑f - Equiv.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (f : α ≃ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f - AddMonoidHom.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f - RingHom.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f - AddEquiv.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Add α] [Add β] (f : α ≃+ β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f - AlgEquiv.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α ≃ₐ[R] β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f - AlgHom.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {R : Type u_7} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (f : α →ₐ[R] β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f - LinearMap.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α →ₗ[R] β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f - AlgEquiv.mopMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] (M : Matrix m m αᵐᵒᵖ) : AlgEquiv.mopMatrix M = MulOpposite.op (M.transpose.map MulOpposite.unop) - AlgEquiv.mopMatrix_symm_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {R : Type u_7} {α : Type v} [Fintype m] [DecidableEq m] [CommSemiring R] [Semiring α] [Algebra R α] (M : (Matrix m m α)ᵐᵒᵖ) : AlgEquiv.mopMatrix.symm M = (MulOpposite.unop M).transpose.map MulOpposite.op - Matrix.map_algebraMap 📋 Mathlib.Data.Matrix.Basic
{n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Fintype n] [DecidableEq n] [CommSemiring R] [Semiring α] [Semiring β] [Algebra R α] [Algebra R β] (r : R) (f : α → β) (hf : f 0 = 0) (hf₂ : f ((algebraMap R α) r) = (algebraMap R β) r) : ((algebraMap R (Matrix n n α)) r).map f = (algebraMap R (Matrix n n β)) r - RingEquiv.mopMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {α : Type v} [Fintype m] [NonAssocSemiring α] (M : Matrix m m αᵐᵒᵖ) : RingEquiv.mopMatrix M = MulOpposite.op (M.transpose.map MulOpposite.unop) - LinearEquiv.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} {β : Type w} [Semiring R] [AddCommMonoid α] [AddCommMonoid β] [Module R α] [Module R β] (f : α ≃ₗ[R] β) (M : Matrix m n α) : f.mapMatrix M = M.map ⇑f - RingEquiv.mapMatrix_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {α : Type v} {β : Type w} [Fintype m] [DecidableEq m] [NonAssocSemiring α] [NonAssocSemiring β] (f : α ≃+* β) (M : Matrix m m α) : f.mapMatrix M = M.map ⇑f - RingEquiv.mopMatrix_symm_apply 📋 Mathlib.Data.Matrix.Basic
{m : Type u_2} {α : Type v} [Fintype m] [NonAssocSemiring α] (M : (Matrix m m α)ᵐᵒᵖ) : RingEquiv.mopMatrix.symm M = (MulOpposite.unop M).transpose.map MulOpposite.op - Matrix.map_single 📋 Mathlib.Data.Matrix.Basis
{m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) {β : Type u_8} [Zero β] {F : Type u_9} [FunLike F α β] [ZeroHomClass F α β] (f : F) : (Matrix.single i j a).map ⇑f = Matrix.single i j (f a) - Matrix.map_stdBasisMatrix 📋 Mathlib.Data.Matrix.Basis
{m : Type u_2} {n : Type u_3} {α : Type u_6} [DecidableEq m] [DecidableEq n] [Zero α] (i : m) (j : n) (a : α) {β : Type u_8} [Zero β] {F : Type u_9} [FunLike F α β] [ZeroHomClass F α β] (f : F) : (Matrix.single i j a).map ⇑f = Matrix.single i j (f a) - Matrix.comp_map_map 📋 Mathlib.Data.Matrix.Composition
{I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (R' : Type u_6) (M : Matrix I J (Matrix K L R)) (f : R → R') : (Matrix.comp I J K L R') (M.map fun M' => M'.map f) = ((Matrix.comp I J K L R) M).map f - Matrix.comp_map_transpose 📋 Mathlib.Data.Matrix.Composition
{I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix I J (Matrix K L R)) : (Matrix.comp I J L K R) (M.map fun x => x.transpose) = ((Matrix.comp J I K L R) M.transpose).transpose - Matrix.comp_transpose 📋 Mathlib.Data.Matrix.Composition
{I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix I J (Matrix K L R)) : (Matrix.comp J I K L R) M.transpose = ((Matrix.comp I J L K R) (M.map fun x => x.transpose)).transpose - Matrix.comp_symm_transpose 📋 Mathlib.Data.Matrix.Composition
{I : Type u_1} {J : Type u_2} {K : Type u_3} {L : Type u_4} {R : Type u_5} (M : Matrix (I × K) (J × L) R) : (Matrix.comp J I L K R).symm M.transpose = (((Matrix.comp I J K L R).symm M).map fun x => x.transpose).transpose - Matrix.conjTranspose.eq_1 📋 Mathlib.Data.Matrix.ConjTranspose
{m : Type u_2} {n : Type u_3} {α : Type v} [Star α] (M : Matrix m n α) : M.conjTranspose = M.transpose.map star - Matrix.conjTranspose_map 📋 Mathlib.Data.Matrix.ConjTranspose
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} [Star α] [Star β] {A : Matrix m n α} (f : α → β) (hf : Function.Semiconj f star star) : A.conjTranspose.map f = (A.map f).conjTranspose - Matrix.blockDiag_map 📋 Mathlib.Data.Matrix.Block
{m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (M : Matrix (m × o) (n × o) α) (f : α → β) : (M.map f).blockDiag = fun k => (M.blockDiag k).map f - Matrix.blockDiag'_map 📋 Mathlib.Data.Matrix.Block
{o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {β : Type u_13} (M : Matrix ((i : o) × m' i) ((i : o) × n' i) α) (f : α → β) : (M.map f).blockDiag' = fun k => (M.blockDiag' k).map f - Matrix.map_toSquareBlock 📋 Mathlib.Data.Matrix.Block
{m : Type u_2} {α : Type u_15} {β : Type u_16} (f : α → β) {M : Matrix m m α} {ι : Type u_18} {b : m → ι} {i : ι} : (M.map f).toSquareBlock b i = (M.toSquareBlock b i).map f - Matrix.blockDiagonal_map 📋 Mathlib.Data.Matrix.Block
{m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} [DecidableEq o] [Zero α] [Zero β] (M : o → Matrix m n α) (f : α → β) (hf : f 0 = 0) : (Matrix.blockDiagonal M).map f = Matrix.blockDiagonal fun k => (M k).map f - Matrix.fromBlocks_map 📋 Mathlib.Data.Matrix.Block
{l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (A : Matrix n l α) (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : α → β) : (Matrix.fromBlocks A B C D).map f = Matrix.fromBlocks (A.map f) (B.map f) (C.map f) (D.map f) - Matrix.blockDiagonal'_map 📋 Mathlib.Data.Matrix.Block
{o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {β : Type u_13} [DecidableEq o] [Zero α] [Zero β] (M : (i : o) → Matrix (m' i) (n' i) α) (f : α → β) (hf : f 0 = 0) : (Matrix.blockDiagonal' M).map f = Matrix.blockDiagonal' fun k => (M k).map f - Matrix.map_updateCol 📋 Mathlib.Data.Matrix.RowCol
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {j : n} {c : m → α} [DecidableEq n] (f : α → β) : (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c) - Matrix.map_updateColumn 📋 Mathlib.Data.Matrix.RowCol
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {j : n} {c : m → α} [DecidableEq n] (f : α → β) : (M.updateCol j c).map f = (M.map f).updateCol j (f ∘ c) - Matrix.map_updateRow 📋 Mathlib.Data.Matrix.RowCol
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} {M : Matrix m n α} {i : m} {b : n → α} [DecidableEq m] (f : α → β) : (M.updateRow i b).map f = (M.map f).updateRow i (f ∘ b) - LinearMap.restrictScalars_toMatrix 📋 Mathlib.LinearAlgebra.Matrix.ToLin
{R : Type u_1} [CommSemiring R] {m : Type u_3} [Fintype m] [DecidableEq m] {A : Type u_4} {M : Type u_5} {n : Type u_6} [Fintype n] [DecidableEq n] [CommSemiring A] [AddCommMonoid M] [Module R M] [Module A M] [Algebra R A] [IsScalarTower R A M] (bA : Basis m R A) (bM : Basis n A M) (f : M →ₗ[A] M) : (LinearMap.toMatrix (bA.smulTower' bM) (bA.smulTower' bM)) (↑R f) = (Matrix.comp n n m m R) (((LinearMap.toMatrix bM bM) f).map ⇑(Algebra.leftMulMatrix bA)) - Int.cast_det 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Basic
{n : Type u_2} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (M : Matrix n n ℤ) : ↑M.det = (M.map fun x => ↑x).det - Rat.cast_det 📋 Mathlib.LinearAlgebra.Matrix.Determinant.Basic
{n : Type u_2} [DecidableEq n] [Fintype n] {F : Type u_3} [Field F] [CharZero F] (M : Matrix n n ℚ) : ↑M.det = (M.map fun x => ↑x).det - Basis.toMatrix_map_vecMul 📋 Mathlib.LinearAlgebra.Matrix.Basis
{ι : Type u_1} {ι' : Type u_2} {R : Type u_5} [CommSemiring R] {S : Type u_9} [Semiring S] [Algebra R S] [Fintype ι] (b : Basis ι R S) (v : ι' → S) : Matrix.vecMul (⇑b) ((b.toMatrix v).map ⇑(algebraMap R S)) = v - Matrix.mvPolynomialX_map_eval₂ 📋 Mathlib.LinearAlgebra.Matrix.MvPolynomial
{m : Type u_1} {n : Type u_2} {R : Type u_3} {S : Type u_4} [CommSemiring R] [CommSemiring S] (f : R →+* S) (A : Matrix m n S) : (Matrix.mvPolynomialX m n R).map (MvPolynomial.eval₂ f fun p => A p.1 p.2) = A - Polynomial.leadingCoeff_det_X_one_add_C 📋 Mathlib.LinearAlgebra.Matrix.Polynomial
{n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) : (Polynomial.X • 1 + A.map ⇑Polynomial.C).det.leadingCoeff = 1 - Polynomial.natDegree_det_X_add_C_le 📋 Mathlib.LinearAlgebra.Matrix.Polynomial
{n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (A B : Matrix n n α) : (Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.natDegree ≤ Fintype.card n - Polynomial.coeff_det_X_add_C_card 📋 Mathlib.LinearAlgebra.Matrix.Polynomial
{n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (A B : Matrix n n α) : (Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.coeff (Fintype.card n) = A.det - Polynomial.coeff_det_X_add_C_zero 📋 Mathlib.LinearAlgebra.Matrix.Polynomial
{n : Type u_1} {α : Type u_2} [DecidableEq n] [Fintype n] [CommRing α] (A B : Matrix n n α) : (Polynomial.X • A.map ⇑Polynomial.C + B.map ⇑Polynomial.C).det.coeff 0 = B.det - Matrix.kroneckerMap_map_left 📋 Mathlib.Data.Matrix.Kronecker
{α : Type u_2} {α' : Type u_3} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α' → β → γ) (g : α → α') (A : Matrix l m α) (B : Matrix n p β) : Matrix.kroneckerMap f (A.map g) B = Matrix.kroneckerMap (fun a b => f (g a) b) A B - Matrix.kroneckerMap_map_right 📋 Mathlib.Data.Matrix.Kronecker
{α : Type u_2} {β : Type u_4} {β' : Type u_5} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α → β' → γ) (g : β → β') (A : Matrix l m α) (B : Matrix n p β) : Matrix.kroneckerMap f A (B.map g) = Matrix.kroneckerMap (fun a b => f a (g b)) A B - Matrix.kroneckerMap_map 📋 Mathlib.Data.Matrix.Kronecker
{α : Type u_2} {β : Type u_4} {γ : Type u_6} {γ' : Type u_7} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} (f : α → β → γ) (g : γ → γ') (A : Matrix l m α) (B : Matrix n p β) : (Matrix.kroneckerMap f A B).map g = Matrix.kroneckerMap (fun a b => g (f a b)) A B - Matrix.kroneckerMap_diagonal_right 📋 Mathlib.Data.Matrix.Kronecker
{α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} [Zero β] [Zero γ] [DecidableEq n] (f : α → β → γ) (hf : ∀ (a : α), f a 0 = 0) (A : Matrix l m α) (b : n → β) : Matrix.kroneckerMap f A (Matrix.diagonal b) = Matrix.blockDiagonal fun i => A.map fun a => f a (b i) - Matrix.kroneckerTMul_diagonal 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [CommSemiring R] [AddCommMonoid α] [Module R α] [DecidableEq n] (A : Matrix l m α) (b : n → α) : Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.diagonal b) = Matrix.blockDiagonal fun i => A.map fun a => a ⊗ₜ[R] b i - Matrix.kroneckerMap_diagonal_left 📋 Mathlib.Data.Matrix.Kronecker
{α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} [Zero α] [Zero γ] [DecidableEq l] (f : α → β → γ) (hf : ∀ (b : β), f 0 b = 0) (a : l → α) (B : Matrix m n β) : Matrix.kroneckerMap f (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun i => B.map fun b => f (a i) b) - Matrix.diagonal_kroneckerTMul 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_2} {l : Type u_8} {m : Type u_9} {n : Type u_10} [CommSemiring R] [AddCommMonoid α] [Module R α] [DecidableEq l] (a : l → α) (B : Matrix m n α) : Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.diagonal a) B = (Matrix.reindex (Equiv.prodComm m l) (Equiv.prodComm n l)) (Matrix.blockDiagonal fun i => B.map fun b => a i ⊗ₜ[R] b) - Matrix.kroneckerTMul_assoc' 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) : ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map ⇑(TensorProduct.assoc R α β γ)).submatrix ⇑(Equiv.prodAssoc l n q).symm ⇑(Equiv.prodAssoc m p r).symm = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C) - Matrix.kroneckerTMul_assoc 📋 Mathlib.Data.Matrix.Kronecker
(R : Type u_1) {α : Type u_2} {β : Type u_4} {γ : Type u_6} {l : Type u_8} {m : Type u_9} {n : Type u_10} {p : Type u_11} {q : Type u_12} {r : Type u_13} [CommSemiring R] [AddCommMonoid α] [AddCommMonoid β] [AddCommMonoid γ] [Module R α] [Module R β] [Module R γ] (A : Matrix l m α) (B : Matrix n p β) (C : Matrix q r γ) : (Matrix.reindex (Equiv.prodAssoc l n q) (Equiv.prodAssoc m p r)) ((Matrix.kroneckerMap (TensorProduct.tmul R) (Matrix.kroneckerMap (TensorProduct.tmul R) A B) C).map ⇑(TensorProduct.assoc R α β γ)) = Matrix.kroneckerMap (TensorProduct.tmul R) A (Matrix.kroneckerMap (TensorProduct.tmul R) B C) - Matrix.det_kroneckerMapBilinear 📋 Mathlib.Data.Matrix.Kronecker
{R : Type u_1} {α : Type u_2} {β : Type u_4} {γ : Type u_6} {m : Type u_9} {n : Type u_10} [CommSemiring R] [Fintype m] [Fintype n] [DecidableEq m] [DecidableEq n] [NonAssocSemiring α] [NonAssocSemiring β] [CommRing γ] [Module R α] [Module R β] [Module R γ] (f : α →ₗ[R] β →ₗ[R] γ) (h_comm : ∀ (a b : α) (a' b' : β), (f (a * b)) (a' * b') = (f a) a' * (f b) b') (A : Matrix m m α) (B : Matrix n n β) : (((Matrix.kroneckerMapBilinear f) A) B).det = (A.map fun a => (f a) 1).det ^ Fintype.card n * (B.map fun b => (f 1) b).det ^ Fintype.card m - Matrix.SpecialLinearGroup.coe_matrix_coe 📋 Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
{n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] (g : Matrix.SpecialLinearGroup n ℤ) : ↑((Matrix.SpecialLinearGroup.map (Int.castRingHom R)) g) = (↑g).map ⇑(Int.castRingHom R) - Matrix.GeneralLinearGroup.coe_map_inv_mul_map 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
{n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) : (↑g)⁻¹.map ⇑f * (↑g).map ⇑f = 1 - Matrix.GeneralLinearGroup.coe_map_mul_map_inv 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
{n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (g : GL n R) : (↑g).map ⇑f * (↑g)⁻¹.map ⇑f = 1 - Matrix.GeneralLinearGroup.val_map_apply 📋 Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
{n : Type u} [DecidableEq n] [Fintype n] {R : Type v} [CommRing R] {S : Type u_1} [CommRing S] (f : R →+* S) (u : (Matrix n n R)ˣ) : ↑((Matrix.GeneralLinearGroup.map f) u) = (↑u).map ⇑f - Matrix.IsSymm.map 📋 Mathlib.LinearAlgebra.Matrix.Symmetric
{α : Type u_1} {β : Type u_2} {n : Type u_3} {A : Matrix n n α} (h : A.IsSymm) (f : α → β) : (A.map f).IsSymm - Matrix.BlockTriangular.map 📋 Mathlib.LinearAlgebra.Matrix.Block
{α : Type u_1} {m : Type u_3} {R : Type v} {M : Matrix m m R} {b : m → α} [LT α] {S : Type u_8} {F : Type u_9} [FunLike F R S] [Zero R] [Zero S] [ZeroHomClass F R S] (f : F) (h : M.BlockTriangular b) : (M.map ⇑f).BlockTriangular b - MatrixEquivTensor.invFun_algebraMap 📋 Mathlib.RingTheory.MatrixAlgebra
(n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (M : Matrix n n R) : MatrixEquivTensor.invFun n R A (M.map ⇑(algebraMap R A)) = 1 ⊗ₜ[R] M - MatrixEquivTensor.toFunAlgHom_apply 📋 Mathlib.RingTheory.MatrixAlgebra
(n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [DecidableEq n] [Fintype n] (a : A) (m : Matrix n n R) : (MatrixEquivTensor.toFunAlgHom n R A) (a ⊗ₜ[R] m) = a • m.map ⇑(algebraMap R A) - matrixEquivTensor_apply_symm 📋 Mathlib.RingTheory.MatrixAlgebra
(n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] [Fintype n] [DecidableEq n] (a : A) (M : Matrix n n R) : (matrixEquivTensor n R A).symm (a ⊗ₜ[R] M) = a • M.map ⇑(algebraMap R A) - MatrixEquivTensor.toFunBilinear_apply 📋 Mathlib.RingTheory.MatrixAlgebra
(n : Type u_3) (R : Type u_5) (A : Type u_6) [CommSemiring R] [Semiring A] [Algebra R A] (a : A) (m : Matrix n n R) : ((MatrixEquivTensor.toFunBilinear n R A) a) m = a • m.map ⇑(algebraMap R A) - matPolyEquiv_map_C 📋 Mathlib.RingTheory.MatrixPolynomialAlgebra
{R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) : matPolyEquiv (M.map ⇑Polynomial.C) = Polynomial.C M - matPolyEquiv_symm_C 📋 Mathlib.RingTheory.MatrixPolynomialAlgebra
{R : Type u_1} [CommSemiring R] {n : Type w} [DecidableEq n] [Fintype n] (M : Matrix n n R) : matPolyEquiv.symm (Polynomial.C M) = M.map ⇑Polynomial.C - Matrix.charpoly_map 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
{R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (f : R →+* S) : (M.map ⇑f).charpoly = Polynomial.map f M.charpoly - Matrix.charmatrix_map 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
{R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] {n : Type u_4} [DecidableEq n] [Fintype n] (M : Matrix n n R) (f : R →+* S) : (M.map ⇑f).charmatrix = M.charmatrix.map (Polynomial.map f) - Matrix.charmatrix_fromBlocks 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
{R : Type u_1} [CommRing R] {m : Type u_3} {n : Type u_4} [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] (M₁₁ : Matrix m m R) (M₁₂ : Matrix m n R) (M₂₁ : Matrix n m R) (M₂₂ : Matrix n n R) : (Matrix.fromBlocks M₁₁ M₁₂ M₂₁ M₂₂).charmatrix = Matrix.fromBlocks M₁₁.charmatrix (-M₁₂.map ⇑Polynomial.C) (-M₂₁.map ⇑Polynomial.C) M₂₂.charmatrix - Matrix.charpolyRev.eq_1 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : M.charpolyRev = (1 - Polynomial.X • M.map ⇑Polynomial.C).det - Matrix.coeff_det_one_add_X_smul_one 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : (1 + Polynomial.X • M.map ⇑Polynomial.C).det.coeff 1 = M.trace - Matrix.eval_det_add_X_smul 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (A : Matrix n n (Polynomial R)) (M : Matrix n n R) : Polynomial.eval 0 (A + Polynomial.X • M.map ⇑Polynomial.C).det = Polynomial.eval 0 A.det - Matrix.matPolyEquiv_eval_eq_map 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n (Polynomial R)) (r : R) : Polynomial.eval ((Matrix.scalar n) r) (matPolyEquiv M) = M.map (Polynomial.eval r) - Matrix.matPolyEquiv_symm_map_eval 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Polynomial (Matrix n n R)) (r : R) : (matPolyEquiv.symm M).map (Polynomial.eval r) = Polynomial.eval ((Matrix.scalar n) r) M - Matrix.det_one_add_smul 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (r : R) (M : Matrix n n R) : (1 + r • M).det = 1 + M.trace * r + Polynomial.eval r (1 + Polynomial.X • M.map ⇑Polynomial.C).det.divX.divX * r ^ 2 - Matrix.derivative_det_one_add_X_smul 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace - Matrix.derivative_det_one_add_X_smul_aux 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : ℕ} (M : Matrix (Fin n) (Fin n) R) : Polynomial.eval 0 (Polynomial.derivative (1 + Polynomial.X • M.map ⇑Polynomial.C).det) = M.trace - Matrix.det_one_add_X_smul 📋 Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
{R : Type u} [CommRing R] {n : Type v} [DecidableEq n] [Fintype n] (M : Matrix n n R) : (1 + Polynomial.X • M.map ⇑Polynomial.C).det = 1 + M.trace • Polynomial.X + (1 + Polynomial.X • M.map ⇑Polynomial.C).det.divX.divX * Polynomial.X ^ 2 - LinearMap.toMatrix_baseChange 📋 Mathlib.RingTheory.TensorProduct.Free
{R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι : Type u_4} {ι₂ : Type u_5} (A : Type u_6) [Fintype ι] [Finite ι₂] [DecidableEq ι] [CommSemiring R] [CommSemiring A] [Algebra R A] [AddCommMonoid M₁] [Module R M₁] [AddCommMonoid M₂] [Module R M₂] (f : M₁ →ₗ[R] M₂) (b₁ : Basis ι R M₁) (b₂ : Basis ι₂ R M₂) : (LinearMap.toMatrix (Algebra.TensorProduct.basis A b₁) (Algebra.TensorProduct.basis A b₂)) (LinearMap.baseChange A f) = ((LinearMap.toMatrix b₁ b₂) f).map ⇑(algebraMap R A) - Matrix.toMvPolynomial_map 📋 Mathlib.Algebra.Module.LinearMap.Polynomial
{m : Type u_1} {n : Type u_2} {R : Type u_4} {S : Type u_5} [Fintype n] [CommSemiring R] [CommSemiring S] (f : R →+* S) (M : Matrix m n R) (i : m) : (M.map ⇑f).toMvPolynomial i = (MvPolynomial.map f) (M.toMvPolynomial i) - Matrix.map.eq_1 📋 Mathlib.LinearAlgebra.Matrix.BaseChange
{m : Type u_2} {n : Type u_3} {α : Type v} {β : Type w} (M : Matrix m n α) (f : α → β) : M.map f = Matrix.of fun i j => f (M i j) - Continuous.matrix_map 📋 Mathlib.Topology.Instances.Matrix
{X : Type u_1} {m : Type u_4} {n : Type u_5} {S : Type u_7} {R : Type u_8} [TopologicalSpace X] [TopologicalSpace R] [TopologicalSpace S] {A : X → Matrix m n S} {f : S → R} (hA : Continuous A) (hf : Continuous f) : Continuous fun x => (A x).map f - Algebra.PreSubmersivePresentation.jacobiMatrix_reindex 📋 Mathlib.RingTheory.Smooth.StandardSmooth
{R : Type u} {S : Type v} [CommRing R] [CommRing S] [Algebra R S] (P : Algebra.PreSubmersivePresentation R S) {ι : Type u_1} {κ : Type u_2} (e : ι ≃ P.vars) (f : κ ≃ P.rels) [Fintype P.rels] [DecidableEq P.rels] [Fintype (P.reindex e f).rels] [DecidableEq (P.reindex e f).rels] : (P.reindex e f).jacobiMatrix = ((Matrix.reindex f.symm f.symm) P.jacobiMatrix).map ⇑(MvPolynomial.rename ⇑e.symm) - Matrix.frobenius_norm_map_eq 📋 Mathlib.Analysis.Matrix
{m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [Fintype m] [Fintype n] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (A : Matrix m n α) (f : α → β) (hf : ∀ (a : α), ‖f a‖ = ‖a‖) : ‖A.map f‖ = ‖A‖ - Matrix.norm_map_eq 📋 Mathlib.Analysis.Matrix
{m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [Fintype m] [Fintype n] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (A : Matrix m n α) (f : α → β) (hf : ∀ (a : α), ‖f a‖ = ‖a‖) : ‖A.map f‖ = ‖A‖ - Matrix.frobenius_nnnorm_map_eq 📋 Mathlib.Analysis.Matrix
{m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [Fintype m] [Fintype n] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (A : Matrix m n α) (f : α → β) (hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊) : ‖A.map f‖₊ = ‖A‖₊ - Matrix.nnnorm_map_eq 📋 Mathlib.Analysis.Matrix
{m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [Fintype m] [Fintype n] [SeminormedAddCommGroup α] [SeminormedAddCommGroup β] (A : Matrix m n α) (f : α → β) (hf : ∀ (a : α), ‖f a‖₊ = ‖a‖₊) : ‖A.map f‖₊ = ‖A‖₊ - CStarMatrix.map_map 📋 Mathlib.Analysis.CStarAlgebra.CStarMatrix
{m : Type u_1} {n : Type u_2} {A : Type u_5} {B : Type u_6} {C : Type u_7} {M : Matrix m n A} {f : A → B} {g : B → C} : (M.map f).map g = M.map (g ∘ f) - PEquiv.map_toMatrix 📋 Mathlib.Data.Matrix.PEquiv
{m : Type u_3} {n : Type u_4} {α : Type u_5} {β : Type u_6} [DecidableEq n] [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (σ : m ≃. n) : σ.toMatrix.map ⇑f = σ.toMatrix - Algebra.traceMatrix_of_matrix_mulVec 📋 Mathlib.RingTheory.Trace.Basic
{κ : Type w} {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype κ] (b : κ → B) (P : Matrix κ κ A) : Algebra.traceMatrix A ((P.map ⇑(algebraMap A B)).mulVec b) = P * Algebra.traceMatrix A b * P.transpose - Algebra.traceMatrix_of_matrix_vecMul 📋 Mathlib.RingTheory.Trace.Basic
{κ : Type w} {A : Type u} {B : Type v} [CommRing A] [CommRing B] [Algebra A B] [Fintype κ] (b : κ → B) (P : Matrix κ κ A) : Algebra.traceMatrix A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.transpose * Algebra.traceMatrix A b * P - 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 - Matrix.IsHermitian.map 📋 Mathlib.LinearAlgebra.Matrix.Hermitian
{α : Type u_1} {β : Type u_2} {n : Type u_4} [Star α] [Star β] {A : Matrix n n α} (h : A.IsHermitian) (f : α → β) (hf : Function.Semiconj f star star) : (A.map f).IsHermitian - Matrix.map_circulant 📋 Mathlib.LinearAlgebra.Matrix.Circulant
{α : Type u_1} {β : Type u_2} {n : Type u_3} [Sub n] (v : n → α) (f : α → β) : (Matrix.circulant v).map f = Matrix.circulant fun i => f (v i) - Matrix.IsDiag.map 📋 Mathlib.LinearAlgebra.Matrix.IsDiag
{α : Type u_1} {β : Type u_2} {n : Type u_4} [Zero α] [Zero β] {A : Matrix n n α} (ha : A.IsDiag) {f : α → β} (hf : f 0 = 0) : (A.map f).IsDiag - Matrix.map_swap 📋 Mathlib.LinearAlgebra.Matrix.Swap
{R : Type u_1} {n : Type u_2} [Semiring R] [DecidableEq n] {S : Type u_4} [NonAssocSemiring S] (f : R →+* S) (i j : n) : (Matrix.swap R i j).map ⇑f = Matrix.swap S i j - RootPairing.Base.cartanMatrixIn_mul_diagonal_eq 📋 Mathlib.LinearAlgebra.RootSystem.CartanMatrix
{ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [CommRing R] [AddCommGroup M] [Module R M] [AddCommGroup N] [Module R N] (S : Type u_5) [CommRing S] [Algebra S R] {P : RootSystem ι R M N} [P.IsValuedIn S] (B : P.InvariantForm) (b : P.Base) [DecidableEq ι] [Fintype ↑b.support] : ((RootPairing.Base.cartanMatrixIn S b).map ⇑(algebraMap S R) * Matrix.diagonal fun i => (B.form (P.root ↑i)) (P.root ↑i)) = 2 • (BilinForm.toMatrix b.toWeightBasis) B.form - Algebra.discr_of_matrix_mulVec 📋 Mathlib.RingTheory.Discriminant
{A : Type u} {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ι → B) (P : Matrix ι ι A) : Algebra.discr A ((P.map ⇑(algebraMap A B)).mulVec b) = P.det ^ 2 * Algebra.discr A b - Algebra.discr_of_matrix_vecMul 📋 Mathlib.RingTheory.Discriminant
{A : Type u} {B : Type v} {ι : Type w} [DecidableEq ι] [CommRing A] [CommRing B] [Algebra A B] [Fintype ι] (b : ι → B) (P : Matrix ι ι A) : Algebra.discr A (Matrix.vecMul b (P.map ⇑(algebraMap A B))) = P.det ^ 2 * Algebra.discr A b - Algebra.Norm.Transitivity.cornerAddX.eq_1 📋 Mathlib.RingTheory.Norm.Transitivity
{S : Type u_2} {m : Type u_5} [CommRing S] (M : Matrix m m S) [DecidableEq m] (k : m) : Algebra.Norm.Transitivity.cornerAddX M k = (Matrix.diagonal fun i => if i = k then Polynomial.X else 0) + M.map ⇑Polynomial.C - Matrix.det_det 📋 Mathlib.RingTheory.Norm.Transitivity
{R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] (M : Matrix m m S) [DecidableEq m] [DecidableEq n] [Fintype m] [Fintype n] (f : S →+* Matrix n n R) : (f M.det).det = ((Matrix.comp m m n n R) (M.map ⇑f)).det - Algebra.Norm.Transitivity.eval_zero_comp_det 📋 Mathlib.RingTheory.Norm.Transitivity
{R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] (M : Matrix m m S) [DecidableEq m] [DecidableEq n] (k : m) [Fintype m] [Fintype n] (f : S →+* Matrix n n R) : Polynomial.eval 0 ((Matrix.comp m m n n (Polynomial R)) ((Algebra.Norm.Transitivity.cornerAddX M k).map ⇑f.polyToMatrix)).det = ((Matrix.comp m m n n R) (M.map ⇑f)).det - Algebra.Norm.Transitivity.comp_det_mul_pow 📋 Mathlib.RingTheory.Norm.Transitivity
{R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] (M : Matrix m m S) [DecidableEq m] [DecidableEq n] (k : m) [Fintype m] [Fintype n] (f : S →+* Matrix n n R) : ((Matrix.comp m m n n R) (M.map ⇑f)).det * (f (M k k)).det ^ (Fintype.card m - 1) = (f (M k k)).det * ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (((M * Algebra.Norm.Transitivity.auxMat M k).toSquareBlock (fun x => x = k) False).map ⇑f)).det - Algebra.Norm.Transitivity.det_det_aux 📋 Mathlib.RingTheory.Norm.Transitivity
{R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [CommRing R] [CommRing S] {M : Matrix m m S} [DecidableEq m] [DecidableEq n] (k : m) [Fintype m] [Fintype n] {f : S →+* Matrix n n R} (ih : ∀ (M : Matrix { a // (a = k) = False } { a // (a = k) = False } S), (f M.det).det = ((Matrix.comp { a // (a = k) = False } { a // (a = k) = False } n n R) (M.map ⇑f)).det) : ((f M.det).det - ((Matrix.comp m m n n R) (M.map ⇑f)).det) * (f (M k k)).det ^ (Fintype.card m - 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 ?aIf 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 ?bBy 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_tsumeven though the hypothesisf i < g iis 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 19971e9 serving mathlib revision bce1d65