_example

Mathlib.Data.Matrix.Reflection

URI: https://scilib.ai/kg/mathlib#Matrix._example

Lean4

example (P : Matrix (Fin 2) (Fin 3) α → Prop) : (∀ x, P x) ↔ ∀ a b c d e f, P !![a, b, c; d, e, f] :=
  (forall_iff _).symm

Похожие утверждения

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru