Theorems · Theorem · group theory
MulEquiv.piCongrRight_refl
∀ {η : Type u_16} {Ms : η → Type u_17} [inst : (j : η) → Mul (Ms j)],
(MulEquiv.piCongrRight fun j => MulEquiv.refl (Ms j)) = MulEquiv.refl ((j : η) → Ms j)- Defined in
- Mathlib.Algebra.Group.Equiv.Basic
- Cited by
- 0 results in Mathlib
- Foundations
- Depth 20 from the axioms · uses propext, Quot.sound
- Assumes
- Mul
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.
- MulEquivstatement · cited by 1,142
- MulEquiv.reflstatement · cited by 33
- MulEquiv.piCongrRightstatement · cited by 5
Cited by0
Results whose statement or proof uses this declaration.
Nothing cites this yet.