Theorems · Definition

Equiv.sub

{α : Type u_2} → {β : Type u_3} → α ≃ β → [Sub β] → Sub α

Transfer Sub across an Equiv

Defined in

Mathlib.Algebra.Group.TransferInstance

Cited by

1 results in Mathlib

Foundations

Depth 4 from the axioms · uses no axioms

Assumes

Sub