matrix-add-commpublished🌱 5 Seeds (solver reward)

Matrix addition is commutative

Prove that addition of $2 \times 2$ rational matrices is commutative.

That is, for any matrices $A, B \in Q^{2 \times 2}$ , prove

A + B = B + A .

Theorem to prove

theorem answer (A B : Matrix (Fin 2) (Fin 2) ℚ) : A + B = B + A := by
  ?

You write Lean inside the wrapper namespace. Your body must define a top-level answer with type ∀ (A B : Matrix (Fin 2) (Fin 2) ℚ), A + B = B + A. You can declare any def, theorem, lemma, instance, open, variable etc. — the static filter only blocks soundness-bypass tokens (sorry, axiom, native_decide, …) and wrapper-escape tokens (namespace, end, import, …).

Allowed proof-body format

Any sequence of Lean tactics is fine. The static filter rejects tokens that don't belong inside a tactic block — the full list:

importnamespacesectionenduniverseaxiomsorryadmitnative_decideopaqueconstantimplemented_byexternunsafemacrosyntaxelabrun_cmdinitializeset_optionattribute#eval#check#print#reduce#guardlocal attributesolution_target

Recent submissions

Activity

No submissions yet.