Mathlib Map

Theorems · Theorem · group theory

Units.val_copy

∀ {α : Type u} [inst : Monoid α] (u : αˣ) (val : α) (hv : val = ↑u) (inv : α) (hi : inv = ↑u⁻¹),
  ↑(u.copy val hv inv hi) = val
Defined in
Mathlib.Algebra.Group.Units.Defs
Cited by
1 results in Mathlib
Foundations
Depth 10 from the axioms · uses no axioms
Assumes
Monoid
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

analyticAt_inverse · cited by 3analyticAt_inverseMonoid · cited by 3887MonoidUnits · cited by 2804UnitsUnits.val · cited by 1966Units.valUnits.copy · cited by 5Units.copyUnits.val_copyCITED BYCITES

Cites4

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

  • Monoidstatement and proof · cited by 3,887
  • Unitsstatement and proof · cited by 2,804
  • Units.valstatement and proof · cited by 1,966
  • Units.copystatement and proof · cited by 5

Cited by1

Results whose statement or proof uses this declaration.