Prod

📁 Source: Mathlib/Algebra/Lie/Prod.lean

Statistics

Metric	Count
Definitions `instLieAlgebra`, `instLieRing`, `fst`, `inl`, `inr`, `prod`, `prodMap`, `snd`	8
Theorems `bracket_apply`, `coe_fst`, `coe_inl`, `coe_inr`, `coe_prod`, `coe_prodMap`, `coe_snd`, `fst_apply`, `fst_comp_inl`, `fst_comp_inr`, `fst_prod`, `fst_surjective`, `inl_apply`, `inl_eq_prod`, `inl_injective`, `inr_apply`, `inr_eq_prod`, `inr_injective`, `ker_fst`, `ker_snd`, `pair_fst_snd`, `prodMap_apply`, `prodMap_comp`, `prodMap_id`, `prodMap_one`, `prodMap_zero`, `prod_apply`, `prod_comp`, `prod_ext`, `prod_ext_iff`, `range_inl`, `range_inr`, `snd_apply`, `snd_comp_inl`, `snd_comp_inr`, `snd_prod`, `snd_surjective`	37
Total	45

LieAlgebra.Prod

Definitions

Name	Category	Theorems
`instLieAlgebra` 📖	CompOp	40 math math: `LieHom.inl_apply`, `LieHom.prodMap_apply`, `LieHom.ker_snd`, `LieHom.snd_prod`, `LieHom.fst_comp_inr`, `LieHom.prodMap_id`, `LieHom.snd_comp_inr`, `LieHom.pair_fst_snd`, `LieHom.snd_comp_inl`, `LieHom.inl_injective`, `LieHom.coe_inl`, `Derivation.Compatible.mem`, `LieHom.fst_surjective`, `LieAlgebra.SemiDirectSum.prod_iso_toFun`, `LieHom.fst_prod`, `Derivation.Compatible.apply`, `LieHom.range_inr`, `LieHom.prodMap_comp`, `LieHom.prodMap_zero`, `LieHom.prod_comp`, `LieHom.prod_apply`, `LieHom.prodMap_one`, `LieHom.range_inl`, `LieHom.prod_ext_iff`, `LieHom.inr_apply`, `LieHom.ker_fst`, `LieHom.inr_injective`, `LieHom.fst_comp_inl`, `LieAlgebra.SemiDirectSum.prod_iso_invFun_left`, `LieHom.fst_apply`, `LieHom.coe_prod`, `LieHom.snd_surjective`, `LieAlgebra.SemiDirectSum.prod_iso_invFun_right`, `Derivation.Compatible.mk_left`, `LieHom.coe_snd`, `LieHom.coe_fst`, `LieHom.coe_inr`, `Derivation.Compatible.mk_right`, `LieHom.coe_prodMap`, `LieHom.snd_apply`
`instLieRing` 📖	CompOp	41 math math: `LieHom.inl_apply`, `LieHom.prodMap_apply`, `LieHom.ker_snd`, `LieHom.snd_prod`, `LieHom.fst_comp_inr`, `LieHom.prodMap_id`, `LieHom.snd_comp_inr`, `LieHom.pair_fst_snd`, `LieHom.snd_comp_inl`, `LieHom.inl_injective`, `LieHom.coe_inl`, `Derivation.Compatible.mem`, `bracket_apply`, `LieHom.fst_surjective`, `LieAlgebra.SemiDirectSum.prod_iso_toFun`, `LieHom.fst_prod`, `Derivation.Compatible.apply`, `LieHom.range_inr`, `LieHom.prodMap_comp`, `LieHom.prodMap_zero`, `LieHom.prod_comp`, `LieHom.prod_apply`, `LieHom.prodMap_one`, `LieHom.range_inl`, `LieHom.prod_ext_iff`, `LieHom.inr_apply`, `LieHom.ker_fst`, `LieHom.inr_injective`, `LieHom.fst_comp_inl`, `LieAlgebra.SemiDirectSum.prod_iso_invFun_left`, `LieHom.fst_apply`, `LieHom.coe_prod`, `LieHom.snd_surjective`, `LieAlgebra.SemiDirectSum.prod_iso_invFun_right`, `Derivation.Compatible.mk_left`, `LieHom.coe_snd`, `LieHom.coe_fst`, `LieHom.coe_inr`, `Derivation.Compatible.mk_right`, `LieHom.coe_prodMap`, `LieHom.snd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`bracket_apply` 📖	mathematical	—	`Bracket.bracket` `LieRingModule.toBracket` `instLieRing` `LieRing.toAddCommGroup` `lieRingSelfModule`	—	—

LieHom

Definitions

Name	Category	Theorems
`fst` 📖	CompOp	9 math math: `fst_comp_inr`, `pair_fst_snd`, `fst_surjective`, `fst_prod`, `range_inr`, `ker_fst`, `fst_comp_inl`, `fst_apply`, `coe_fst`
`inl` 📖	CompOp	9 math math: `inl_apply`, `ker_snd`, `snd_comp_inl`, `inl_injective`, `coe_inl`, `inl_eq_prod`, `range_inl`, `prod_ext_iff`, `fst_comp_inl`
`inr` 📖	CompOp	9 math math: `fst_comp_inr`, `snd_comp_inr`, `inr_eq_prod`, `range_inr`, `prod_ext_iff`, `inr_apply`, `ker_fst`, `inr_injective`, `coe_inr`
`prod` 📖	CompOp	8 math math: `snd_prod`, `pair_fst_snd`, `inr_eq_prod`, `inl_eq_prod`, `fst_prod`, `prod_comp`, `prod_apply`, `coe_prod`
`prodMap` 📖	CompOp	6 math math: `prodMap_apply`, `prodMap_id`, `prodMap_comp`, `prodMap_zero`, `prodMap_one`, `coe_prodMap`
`snd` 📖	CompOp	9 math math: `ker_snd`, `snd_prod`, `snd_comp_inr`, `pair_fst_snd`, `snd_comp_inl`, `range_inl`, `snd_surjective`, `coe_snd`, `snd_apply`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`coe_fst` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `fst`	—	—
`coe_inl` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	—
`coe_inr` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `inr` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	—
`coe_prod` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `prod` `Pi.prod`	—	—
`coe_prodMap` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `prodMap`	—	—
`coe_snd` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `snd`	—	—
`fst_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `fst`	—	—
`fst_comp_inl` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `fst` `inl` `id`	—	—
`fst_comp_inr` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `fst` `inr` `LieHom` `instZero`	—	—
`fst_prod` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `fst` `prod`	—	—
`fst_surjective` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `fst`	—	—
`inl_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `inl` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	—
`inl_eq_prod` 📖	mathematical	—	`inl` `prod` `id` `LieHom` `instZero`	—	—
`inl_injective` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `inl`	—	—
`inr_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `inr` `NegZeroClass.toZero` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `SubtractionCommMonoid.toSubtractionMonoid` `AddCommGroup.toDivisionAddCommMonoid` `LieRing.toAddCommGroup`	—	—
`inr_eq_prod` 📖	mathematical	—	`inr` `prod` `LieHom` `instZero` `id`	—	—
`inr_injective` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `inr`	—	—
`ker_fst` 📖	mathematical	—	`LieIdeal.toLieSubalgebra` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `ker` `fst` `range` `inr`	—	`range_inr`
`ker_snd` 📖	mathematical	—	`LieIdeal.toLieSubalgebra` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `ker` `snd` `range` `inl`	—	`range_inl`
`pair_fst_snd` 📖	mathematical	—	`prod` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `fst` `snd` `id`	—	—
`prodMap_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `prodMap`	—	—
`prodMap_comp` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `prodMap`	—	—
`prodMap_id` 📖	mathematical	—	`prodMap` `id` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra`	—	—
`prodMap_one` 📖	mathematical	—	`prodMap` `LieHom` `instOne` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra`	—	—
`prodMap_zero` 📖	mathematical	—	`prodMap` `LieHom` `instZero` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra`	—	—
`prod_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `prod`	—	—
`prod_comp` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `prod`	—	—
`prod_ext` 📖	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `inl` `inr`	—	—	`prod_ext_iff`
`prod_ext_iff` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `inl` `inr`	—	`RingHomCompTriple.ids` `LinearMap.prod_ext_iff`
`range_inl` 📖	mathematical	—	`range` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `inl` `LieIdeal.toLieSubalgebra` `ker` `snd`	—	`RingHomSurjective.ids` `range_toSubmodule` `LieIdeal.toLieSubalgebra_toSubmodule` `ker_toSubmodule` `LinearMap.range_inl`
`range_inr` 📖	mathematical	—	`range` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `inr` `LieIdeal.toLieSubalgebra` `ker` `fst`	—	`RingHomSurjective.ids` `range_toSubmodule` `LieIdeal.toLieSubalgebra_toSubmodule` `ker_toSubmodule` `LinearMap.range_inr`
`snd_apply` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `snd`	—	—
`snd_comp_inl` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `snd` `inl` `LieHom` `instZero`	—	—
`snd_comp_inr` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `snd` `inr` `id`	—	—
`snd_prod` 📖	mathematical	—	`comp` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `snd` `prod`	—	—
`snd_surjective` 📖	mathematical	—	`DFunLike.coe` `LieHom` `LieAlgebra.Prod.instLieRing` `LieAlgebra.Prod.instLieAlgebra` `instFunLike` `snd`	—	—

---

← Back to Index