Mathlib Map

Theorems · Theorem · group theory

List.prod_isUnit

∀ {M : Type u_4} [inst : Monoid M] {L : List M}, (∀ m ∈ L, IsUnit m) → IsUnit L.prod
Defined in
Mathlib.Algebra.BigOperators.Group.List.Lemmas
Cited by
2 results in Mathlib
Foundations
Depth 11 from the axioms · uses propext
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

Dashed lines are statement dependencies; solid lines are citations in proofs.

spectrum.exists_mem_of_not_isUnit_aeval_prod · cited by 2spectrum.exists_mem_of_no…List.prod_isUnit_iff · cited by 1List.prod_isUnit_iffMonoid · cited by 3887MonoidIsUnit · cited by 1602IsUnitList.prod_isUnitCITED BYCITES

Cites2

Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.

  • Monoidstatement and proof · cited by 3,887
  • IsUnitstatement and proof · cited by 1,602

Cited by2

Results whose statement or proof uses this declaration.