Mathlib Map

Theorems · Theorem · logic and foundations

eq_comm_eq

∀ {α : Sort u_1} (a b : α), (a = b) = (b = a)
Defined in
Mathlib.Logic.Basic
Cited by
17 results in Mathlib
Foundations
Depth 6 from the axioms · uses propext
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Matrix.diagonal_transpose · cited by 17Matrix.diagonal_transposezero_eq_mul · cited by 6zero_eq_mulFiniteField.orderOf_frobeniusAlgHom · cited by 3FiniteField.orderOf_frobe…LinearMap.exact_zero_iff_surjective · cited by 2LinearMap.exact_zero_iff_…Function.eq_update_self_iff · cited by 2Function.eq_update_self_i…Ordinal.lift_eq_omega_natCast · cited by 1Ordinal.lift_eq_omega_nat…Cardinal.lift_eq_aleph_natCast · cited by 1Cardinal.lift_eq_aleph_na…Cardinal.lift_eq_beth_natCast · cited by 1Cardinal.lift_eq_beth_nat…MvPolynomial.indicator_mem_restrictDegree · cited by 1MvPolynomial.indicator_me…cfcₙ_map_prod · cited by 1cfcₙ_map_prodPi.update_eq_sub_add_single · cited by 1Pi.update_eq_sub_add_sing…Ordinal.lift_eq_omega_one · cited by 0Ordinal.lift_eq_omega_oneCardinal.lift_eq_aleph0 · cited by 0Cardinal.lift_eq_aleph0Cardinal.zero_eq_lift_iff · cited by 0Cardinal.zero_eq_lift_iffCardinal.lift_eq_aleph_one · cited by 0Cardinal.lift_eq_aleph_oneeq_comm_eqCITED BYCITES

Cites0

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

Nothing in Mathlib beyond the foundations.

Cited by17

Results whose statement or proof uses this declaration.