Prod

📁 Source: Mathlib/LinearAlgebra/Basis/Prod.lean

Statistics

Metric	Count
Definitions prod	1
Theorems prod_apply, prod_apply_inl_fst, prod_apply_inl_snd, prod_apply_inr_fst, prod_apply_inr_snd, prod_repr_inl, prod_repr_inr, prod	8
Total	9

Module.Basis

Definitions

Name	Category	Theorems
prod 📖	CompOp	12 math math: Polynomial.toMatrix_sylvesterMap', prod_repr_inl, prod_apply_inr_fst, prod_apply_inl_snd, prod_addHaar, prod_apply, prod_parallelepiped, LinearMap.toMatrix_prodMap, Polynomial.toMatrix_sylvesterMap, prod_apply_inl_fst, prod_repr_inr, prod_apply_inr_snd

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod_apply 📖	mathematical	—	DFunLike.coe Module.Basis Prod.instAddCommMonoid Prod.instModule instFunLike prod LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike LinearMap.inl LinearMap.inr	—	prod_apply_inl_fst prod_apply_inr_fst prod_apply_inl_snd prod_apply_inr_snd
prod_apply_inl_fst 📖	mathematical	—	DFunLike.coe Module.Basis Prod.instAddCommMonoid Prod.instModule instFunLike prod	—	LinearEquiv.injective RingHomInvPair.ids Finsupp.ext LinearEquiv.apply_symm_apply repr_self Finsupp.single_apply_left Sum.inl_injective
prod_apply_inl_snd 📖	mathematical	—	DFunLike.coe Module.Basis Prod.instAddCommMonoid Prod.instModule instFunLike prod AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LinearEquiv.injective RingHomInvPair.ids Finsupp.ext LinearEquiv.apply_symm_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.single_eq_of_ne
prod_apply_inr_fst 📖	mathematical	—	DFunLike.coe Module.Basis Prod.instAddCommMonoid Prod.instModule instFunLike prod AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid	—	LinearEquiv.injective RingHomInvPair.ids Finsupp.ext LinearEquiv.apply_symm_apply map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Finsupp.single_eq_of_ne
prod_apply_inr_snd 📖	mathematical	—	DFunLike.coe Module.Basis Prod.instAddCommMonoid Prod.instModule instFunLike prod	—	LinearEquiv.injective RingHomInvPair.ids Finsupp.ext LinearEquiv.apply_symm_apply repr_self Finsupp.single_apply_left Sum.inr_injective
prod_repr_inl 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Prod.instAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instModule Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr prod	—	RingHomInvPair.ids
prod_repr_inr 📖	mathematical	—	DFunLike.coe Finsupp MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids Prod.instAddCommMonoid Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid Prod.instModule Finsupp.module Semiring.toModule EquivLike.toFunLike LinearEquiv.instEquivLike repr prod	—	RingHomInvPair.ids

Module.Free

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
prod 📖	mathematical	—	Module.Free Prod.instAddCommMonoid Prod.instModule	—	of_basis

---

← Back to Index