Pull an additive subgroup back to an opposite additive subgroup along AddOpposite.unop
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Pull an opposite additive subgroup back to an additive subgroup along AddOpposite.op
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
Lattice results #
theorem
AddSubgroup.op_le_iff
{G : Type u_2}
[AddGroup G]
{S₁ : AddSubgroup G}
{S₂ : AddSubgroup Gᵃᵒᵖ}
:
theorem
AddSubgroup.le_op_iff
{G : Type u_2}
[AddGroup G]
{S₁ : AddSubgroup Gᵃᵒᵖ}
{S₂ : AddSubgroup G}
:
@[simp]
An additive subgroup H
of G
determines an additive subgroup
H.op
of the opposite additive group Gᵃᵒᵖ
.
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
Bijection between an additive subgroup H
and its opposite.
Equations
Instances For
@[simp]
@[simp]
@[simp]
@[simp]
theorem
AddSubgroup.equivOp_symm_apply_coe
{G : Type u_2}
[AddGroup G]
(H : AddSubgroup G)
(b : ↥H.op)
: