Self-inverse elements

This file defines self-inverse elements of a type with an inversion, i.e. elements a satisfying a⁻¹ = a.

Main declarations

• IsSelfInv a: The element a satisfies a⁻¹ = a.
• IsSelfNeg a: The element a satisfies -a = a.

def IsSelfInv {α : Type u_1} [Inv α] (a : α) : Prop

An element a is self-inverse if a⁻¹ = a.

Equations

• IsSelfInv a = (a⁻¹ = a)

def IsSelfNeg {α : Type u_1} [Neg α] (a : α) : Prop

An element a is self-negative if -a = a.

Equations

• IsSelfNeg a = (-a = a)

theorem isSelfInv_iff {α : Type u_1} [Inv α] {a : α} : IsSelfInv a ↔ a⁻¹ = a

theorem isSelfNeg_iff {α : Type u_1} [Neg α] {a : α} : IsSelfNeg a ↔ -a = a

theorem IsSelfInv.inv_eq {α : Type u_1} [Inv α] {a : α} : IsSelfInv a → a⁻¹ = a

Alias of the forward direction of isSelfInv_iff.

theorem IsSelfInv.of_inv_eq {α : Type u_1} [Inv α] {a : α} : a⁻¹ = a → IsSelfInv a

Alias of the reverse direction of isSelfInv_iff.

theorem IsSelfNeg.of_neg_eq {α : Type u_1} [Neg α] {a : α} : -a = a → IsSelfNeg a

Alias of the reverse direction of isSelfNeg_iff.

theorem IsSelfNeg.neg_eq {α : Type u_1} [Neg α] {a : α} : IsSelfNeg a → -a = a

Alias of the forward direction of isSelfNeg_iff.

theorem IsSelfInv.eq_inv {α : Type u_1} [Inv α] {a : α} (h : IsSelfInv a) : a = a⁻¹

theorem IsSelfNeg.eq_neg {α : Type u_1} [Neg α] {a : α} (h : IsSelfNeg a) : a = -a

@[instance_reducible]

instance instDecidableIsSelfInvOfDecidableEq {α : Type u_1} [Inv α] {a : α} [DecidableEq α] : Decidable (IsSelfInv a)

Equations

• instDecidableIsSelfInvOfDecidableEq = decidable_of_iff (a⁻¹ = a) ⋯

@[instance_reducible]

instance instDecidableIsSelfNegOfDecidableEq {α : Type u_1} [Neg α] {a : α} [DecidableEq α] : Decidable (IsSelfNeg a)

Equations

• instDecidableIsSelfNegOfDecidableEq = decidable_of_iff (-a = a) ⋯

@[simp]

theorem IsSelfInv.one {α : Type u_1} [InvOneClass α] : IsSelfInv 1

@[simp]

theorem IsSelfNeg.zero {α : Type u_1} [NegZeroClass α] : IsSelfNeg 0

@[simp]

theorem isSelfInv_inv {α : Type u_1} [InvolutiveInv α] {a : α} : IsSelfInv a⁻¹ ↔ IsSelfInv a

@[simp]

theorem isSelfNeg_neg {α : Type u_1} [InvolutiveNeg α] {a : α} : IsSelfNeg (-a) ↔ IsSelfNeg a

theorem IsSelfInv.inv {α : Type u_1} [InvolutiveInv α] {a : α} : IsSelfInv a → IsSelfInv a⁻¹

Alias of the reverse direction of isSelfInv_inv.

theorem IsSelfNeg.neg {α : Type u_1} [InvolutiveNeg α] {a : α} : IsSelfNeg a → IsSelfNeg (-a)

Alias of the reverse direction of isSelfNeg_neg.

theorem IsSelfInv.conj {α : Type u_1} [DivisionMonoid α] {a : α} (h : IsSelfInv a) (b : α) : IsSelfInv (b * a * b⁻¹)

theorem IsSelfNeg.addConj {α : Type u_1} [SubtractionMonoid α] {a : α} (h : IsSelfNeg a) (b : α) : IsSelfNeg (b + a + -b)

theorem isSelfInv_conj_iff {α : Type u_1} [Group α] {a b : α} : IsSelfInv (b * a * b⁻¹) ↔ IsSelfInv a

theorem isSelfNeg_addConj_iff {α : Type u_1} [AddGroup α] {a b : α} : IsSelfNeg (b + a + -b) ↔ IsSelfNeg a

theorem IsSelfInv.pow {α : Type u_1} [DivisionMonoid α] {a : α} (h : IsSelfInv a) (n : ℕ) : IsSelfInv (a ^ n)

theorem IsSelfNeg.nsmul {α : Type u_1} [SubtractionMonoid α] {a : α} (h : IsSelfNeg a) (n : ℕ) : IsSelfNeg (n • a)

theorem IsSelfInv.zpow {α : Type u_1} [DivisionMonoid α] {a : α} (h : IsSelfInv a) (n : ℤ) : IsSelfInv (a ^ n)

theorem IsSelfNeg.zsmul {α : Type u_1} [SubtractionMonoid α] {a : α} (h : IsSelfNeg a) (n : ℤ) : IsSelfNeg (n • a)

theorem isSelfInv_iff_sq_eq_one {α : Type u_1} [Group α] {a : α} : IsSelfInv a ↔ a ^ 2 = 1

theorem isSelfNeg_iff_two_nsmul_eq_zero {α : Type u_1} [AddGroup α] {a : α} : IsSelfNeg a ↔ 2 • a = 0

theorem IsSelfInv.mul {α : Type u_1} [DivisionCommMonoid α] {a b : α} (ha : IsSelfInv a) (hb : IsSelfInv b) : IsSelfInv (a * b)

theorem IsSelfNeg.add {α : Type u_1} [SubtractionCommMonoid α] {a b : α} (ha : IsSelfNeg a) (hb : IsSelfNeg b) : IsSelfNeg (a + b)

theorem IsSelfInv.div {α : Type u_1} [DivisionCommMonoid α] {a b : α} (ha : IsSelfInv a) (hb : IsSelfInv b) : IsSelfInv (a / b)

theorem IsSelfNeg.sub {α : Type u_1} [SubtractionCommMonoid α] {a b : α} (ha : IsSelfNeg a) (hb : IsSelfNeg b) : IsSelfNeg (a - b)