Mathlib Map

Theorems · Definition · group theory

Submonoid.copy

{M : Type u_1} → [inst : MulOneClass M] → (S : Submonoid M) → (s : Set M) → s = ↑S → Submonoid M

Copy a submonoid replacing carrier with a set that is equal to it.

Defined in
Mathlib.Algebra.Group.Submonoid.Defs
Cited by
4 results in Mathlib
Foundations
Depth 12 from the axioms · uses no axioms
Assumes
MulOneClass
Mathlib docsSourceLoogleLeanSearch

Around this declaration

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

Submonoid.powers · cited by 408Submonoid.powersMonoidHom.mrange · cited by 63MonoidHom.mrangeSubring.mk' · cited by 6Subring.mk'Subsemiring.copy · cited by 5Subsemiring.copySubmonoid.copy_eq · cited by 1Submonoid.copy_eqjacobiSym.trichotomy · cited by 1jacobiSym.trichotomySubmonoid.coe_copy · cited by 0Submonoid.coe_copySubmonoid.copy.congr_simp · cited by 0copy.congr_simpSet · cited by 53352SetSetLike.coe · cited by 8199SetLike.coeSubmonoid · cited by 3086SubmonoidMulOneClass · cited by 1018MulOneClassSubmonoid.copyCITED BYCITES

Cites4

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

  • Setstatement and proof · cited by 53,352
  • SetLike.coestatement and proof · cited by 8,199
  • Submonoidstatement and proof · cited by 3,086
  • MulOneClassstatement and proof · cited by 1,018

Cited by8

Results whose statement or proof uses this declaration.