Theorems · Theorem · group theory

List.eq_of_prod_take_eq

∀ {M : Type u_4} [inst : LeftCancelMonoid M] {L L' : List M},
  L.length = L'.length → (∀ i ≤ L.length, (List.take i L).prod = (List.take i L').prod) → L = L'

Defined in: Mathlib.Algebra.BigOperators.Group.List.Basic
Cited by: 0 results in Mathlib
Foundations: Depth 46 from the axioms · uses propext, Quot.sound
Assumes: LeftCancelMonoid

Mathlib docs Source Loogle LeanSearch

Around this declaration

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

Cites3

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

LeftCancelMonoidstatement and proof · cited by 28
mul_left_cancelproof · cited by 16
List.prod_take_succproof · cited by 3

Cited by0

Results whose statement or proof uses this declaration.

Nothing cites this yet.