group_theory.group_action.basic

source

def mul_action.orbit (α : Type u) {β : Type v} [monoid α] [mul_action α β] (b : β) :

set β

The orbit of an element under an action.

Equations

mul_action.orbit α b = set.range (λ (x : α), x • b)

Instances for ↥mul_action.orbit

source

def add_action.orbit (α : Type u) {β : Type v} [add_monoid α] [add_action α β] (b : β) :

set β

The orbit of an element under an action.

Equations

add_action.orbit α b = set.range (λ (x : α), x +ᵥ b)

Instances for ↥add_action.orbit

source

theorem add_action.mem_orbit_iff {α : Type u} {β : Type v} [add_monoid α] [add_action α β] {b₁ b₂ : β} :

b₂ ∈ add_action.orbit α b₁ ↔ ∃ (x : α), x +ᵥ b₁ = b₂

source

theorem mul_action.mem_orbit_iff {α : Type u} {β : Type v} [monoid α] [mul_action α β] {b₁ b₂ : β} :

b₂ ∈ mul_action.orbit α b₁ ↔ ∃ (x : α), x • b₁ = b₂

source

@[simp]

theorem mul_action.mem_orbit {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) (x : α) :

x • b ∈ mul_action.orbit α b

source

@[simp]

theorem add_action.mem_orbit {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) (x : α) :

x +ᵥ b ∈ add_action.orbit α b

source

@[simp]

theorem mul_action.mem_orbit_self {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) :

b ∈ mul_action.orbit α b

source

@[simp]

theorem add_action.mem_orbit_self {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) :

b ∈ add_action.orbit α b

source

theorem mul_action.orbit_nonempty {α : Type u} {β : Type v} [monoid α] [mul_action α β] (b : β) :

(mul_action.orbit α b).nonempty

source

theorem add_action.orbit_nonempty {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (b : β) :

(add_action.orbit α b).nonempty

source

theorem add_action.maps_to_vadd_orbit {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (a : α) (b : β) :

set.maps_to (has_vadd.vadd a) (add_action.orbit α b) (add_action.orbit α b)

source

theorem mul_action.maps_to_smul_orbit {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a : α) (b : β) :

set.maps_to (has_smul.smul a) (mul_action.orbit α b) (mul_action.orbit α b)

source

theorem add_action.vadd_orbit_subset {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (a : α) (b : β) :

a +ᵥ add_action.orbit α b ⊆ add_action.orbit α b

source

theorem mul_action.smul_orbit_subset {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a : α) (b : β) :

a • mul_action.orbit α b ⊆ mul_action.orbit α b

source

theorem mul_action.orbit_smul_subset {α : Type u} {β : Type v} [monoid α] [mul_action α β] (a : α) (b : β) :

mul_action.orbit α (a • b) ⊆ mul_action.orbit α b

source

theorem add_action.orbit_vadd_subset {α : Type u} {β : Type v} [add_monoid α] [add_action α β] (a : α) (b : β) :

add_action.orbit α (a +ᵥ b) ⊆ add_action.orbit α b

source

@[protected, instance]

def mul_action.orbit.mul_action {α : Type u} {β : Type v} [monoid α] [mul_action α β] {b : β} :

mul_action α ↥(mul_action.orbit α b)

Equations

mul_action.orbit.mul_action = {to_has_smul := {smul := λ (a : α), set.maps_to.restrict (has_smul.smul a) (mul_action.orbit α b) (mul_action.orbit α b) _}, one_smul := _, mul_smul := _}

source

@[protected, instance]

def add_action.orbit.add_action {α : Type u} {β : Type v} [add_monoid α] [add_action α β] {b : β} :

add_action α ↥(add_action.orbit α b)

Equations

add_action.orbit.add_action = {to_has_vadd := {vadd := λ (a : α), set.maps_to.restrict (has_vadd.vadd a) (add_action.orbit α b) (add_action.orbit α b) _}, zero_vadd := _, add_vadd := _}

source

@[simp]

theorem add_action.orbit.coe_vadd {α : Type u} {β : Type v} [add_monoid α] [add_action α β] {b : β} {a : α} {b' : ↥(add_action.orbit α b)} :

↑(a +ᵥ b') = a +ᵥ ↑b'

source

@[simp]

theorem mul_action.orbit.coe_smul {α : Type u} {β : Type v} [monoid α] [mul_action α β] {b : β} {a : α} {b' : ↥(mul_action.orbit α b)} :

↑(a • b') = a • ↑b'

source

def add_action.fixed_points (α : Type u) (β : Type v) [add_monoid α] [add_action α β] :

set β

The set of elements fixed under the whole action.

Equations

add_action.fixed_points α β = {b : β | ∀ (x : α), x +ᵥ b = b}

source

def mul_action.fixed_points (α : Type u) (β : Type v) [monoid α] [mul_action α β] :

set β

The set of elements fixed under the whole action.

Equations

mul_action.fixed_points α β = {b : β | ∀ (x : α), x • b = b}

source

def add_action.fixed_by (α : Type u) (β : Type v) [add_monoid α] [add_action α β] (g : α) :

set β

fixed_by g is the subfield of elements fixed by g.

Equations

add_action.fixed_by α β g = {x : β | g +ᵥ x = x}

source

def mul_action.fixed_by (α : Type u) (β : Type v) [monoid α] [mul_action α β] (g : α) :

set β

fixed_by g is the subfield of elements fixed by g.

Equations

mul_action.fixed_by α β g = {x : β | g • x = x}

source

theorem mul_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [monoid α] [mul_action α β] :

mul_action.fixed_points α β = ⋂ (g : α), mul_action.fixed_by α β g

source

theorem add_action.fixed_eq_Inter_fixed_by (α : Type u) (β : Type v) [add_monoid α] [add_action α β] :

add_action.fixed_points α β = ⋂ (g : α), add_action.fixed_by α β g

source

@[simp]

theorem mul_action.mem_fixed_points {α : Type u} (β : Type v) [monoid α] [mul_action α β] {b : β} :

b ∈ mul_action.fixed_points α β ↔ ∀ (x : α), x • b = b

source

@[simp]

theorem add_action.mem_fixed_points {α : Type u} (β : Type v) [add_monoid α] [add_action α β] {b : β} :

b ∈ add_action.fixed_points α β ↔ ∀ (x : α), x +ᵥ b = b

source

@[simp]

theorem mul_action.mem_fixed_by {α : Type u} (β : Type v) [monoid α] [mul_action α β] {g : α} {b : β} :

b ∈ mul_action.fixed_by α β g ↔ g • b = b

source

@[simp]

theorem add_action.mem_fixed_by {α : Type u} (β : Type v) [add_monoid α] [add_action α β] {g : α} {b : β} :

b ∈ add_action.fixed_by α β g ↔ g +ᵥ b = b

source

theorem mul_action.mem_fixed_points' {α : Type u} (β : Type v) [monoid α] [mul_action α β] {b : β} :

b ∈ mul_action.fixed_points α β ↔ ∀ (b' : β), b' ∈ mul_action.orbit α b → b' = b

source

theorem add_action.mem_fixed_points' {α : Type u} (β : Type v) [add_monoid α] [add_action α β] {b : β} :

b ∈ add_action.fixed_points α β ↔ ∀ (b' : β), b' ∈ add_action.orbit α b → b' = b

source

def mul_action.stabilizer.submonoid (α : Type u) {β : Type v} [monoid α] [mul_action α β] (b : β) :

submonoid α

The stabilizer of a point b as a submonoid of α.

Equations

mul_action.stabilizer.submonoid α b = {carrier := {a : α | a • b = b}, mul_mem' := _, one_mem' := _}

source

def add_action.stabilizer.add_submonoid (α : Type u) {β : Type v} [add_monoid α] [add_action α β] (b : β) :

add_submonoid α

The stabilizer of a point b as an additive submonoid of α.

Equations

add_action.stabilizer.add_submonoid α b = {carrier := {a : α | a +ᵥ b = b}, add_mem' := _, zero_mem' := _}

source

@[simp]

theorem add_action.mem_stabilizer_add_submonoid_iff (α : Type u) {β : Type v} [add_monoid α] [add_action α β] {b : β} {a : α} :

a ∈ add_action.stabilizer.add_submonoid α b ↔ a +ᵥ b = b

source

@[simp]

theorem mul_action.mem_stabilizer_submonoid_iff (α : Type u) {β : Type v} [monoid α] [mul_action α β] {b : β} {a : α} :

a ∈ mul_action.stabilizer.submonoid α b ↔ a • b = b

source

theorem add_action.orbit_eq_univ (α : Type u) {β : Type v} [add_monoid α] [add_action α β] [add_action.is_pretransitive α β] (x : β) :

add_action.orbit α x = set.univ

source

theorem mul_action.orbit_eq_univ (α : Type u) {β : Type v} [monoid α] [mul_action α β] [mul_action.is_pretransitive α β] (x : β) :

mul_action.orbit α x = set.univ

source

theorem add_action.mem_fixed_points_iff_card_orbit_eq_zero {α : Type u} {β : Type v} [add_monoid α] [add_action α β] {a : β} [fintype ↥(add_action.orbit α a)] :

a ∈ add_action.fixed_points α β ↔ fintype.card ↥(add_action.orbit α a) = 1

source

theorem mul_action.mem_fixed_points_iff_card_orbit_eq_one {α : Type u} {β : Type v} [monoid α] [mul_action α β] {a : β} [fintype ↥(mul_action.orbit α a)] :

a ∈ mul_action.fixed_points α β ↔ fintype.card ↥(mul_action.orbit α a) = 1

source

def mul_action.stabilizer (α : Type u) {β : Type v} [group α] [mul_action α β] (b : β) :

subgroup α

The stabilizer of an element under an action, i.e. what sends the element to itself. A subgroup.

Equations

mul_action.stabilizer α b = {carrier := (mul_action.stabilizer.submonoid α b).carrier, mul_mem' := _, one_mem' := _, inv_mem' := _}

Instances for ↥mul_action.stabilizer

valuation_subring.decomposition_subgroup_mul_semiring_action

source

def add_action.stabilizer (α : Type u) {β : Type v} [add_group α] [add_action α β] (b : β) :

add_subgroup α

The stabilizer of an element under an action, i.e. what sends the element to itself. An additive subgroup.

Equations

add_action.stabilizer α b = {carrier := (add_action.stabilizer.add_submonoid α b).carrier, add_mem' := _, zero_mem' := _, neg_mem' := _}

source

@[simp]

theorem add_action.mem_stabilizer_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {b : β} {a : α} :

a ∈ add_action.stabilizer α b ↔ a +ᵥ b = b

source

@[simp]

theorem mul_action.mem_stabilizer_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {b : β} {a : α} :

a ∈ mul_action.stabilizer α b ↔ a • b = b

source

@[simp]

theorem mul_action.smul_orbit {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) (b : β) :

a • mul_action.orbit α b = mul_action.orbit α b

source

@[simp]

theorem add_action.vadd_orbit {α : Type u} {β : Type v} [add_group α] [add_action α β] (a : α) (b : β) :

a +ᵥ add_action.orbit α b = add_action.orbit α b

source

@[simp]

theorem mul_action.orbit_smul {α : Type u} {β : Type v} [group α] [mul_action α β] (a : α) (b : β) :

mul_action.orbit α (a • b) = mul_action.orbit α b

source

@[simp]

theorem add_action.orbit_vadd {α : Type u} {β : Type v} [add_group α] [add_action α β] (a : α) (b : β) :

add_action.orbit α (a +ᵥ b) = add_action.orbit α b

source

@[protected, instance]

def mul_action.orbit.is_pretransitive {α : Type u} {β : Type v} [group α] [mul_action α β] (x : β) :

mul_action.is_pretransitive α ↥(mul_action.orbit α x)

The action of a group on an orbit is transitive.

source

@[protected, instance]

def add_action.orbit.is_pretransitive {α : Type u} {β : Type v} [add_group α] [add_action α β] (x : β) :

add_action.is_pretransitive α ↥(add_action.orbit α x)

The action of an additive group on an orbit is transitive.

source

theorem mul_action.orbit_eq_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {a b : β} :

mul_action.orbit α a = mul_action.orbit α b ↔ a ∈ mul_action.orbit α b

source

theorem add_action.orbit_eq_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {a b : β} :

add_action.orbit α a = add_action.orbit α b ↔ a ∈ add_action.orbit α b

source

theorem add_action.mem_orbit_vadd (α : Type u) {β : Type v} [add_group α] [add_action α β] (g : α) (a : β) :

a ∈ add_action.orbit α (g +ᵥ a)

source

theorem mul_action.mem_orbit_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (g : α) (a : β) :

a ∈ mul_action.orbit α (g • a)

source

theorem mul_action.smul_mem_orbit_smul (α : Type u) {β : Type v} [group α] [mul_action α β] (g h : α) (a : β) :

g • a ∈ mul_action.orbit α (h • a)

source

theorem add_action.vadd_mem_orbit_vadd (α : Type u) {β : Type v} [add_group α] [add_action α β] (g h : α) (a : β) :

g +ᵥ a ∈ add_action.orbit α (h +ᵥ a)

source

def mul_action.orbit_rel (α : Type u) (β : Type v) [group α] [mul_action α β] :

setoid β

The relation 'in the same orbit'.

Equations

mul_action.orbit_rel α β = {r := λ (a b : β), a ∈ mul_action.orbit α b, iseqv := _}

source

def add_action.orbit_rel (α : Type u) (β : Type v) [add_group α] [add_action α β] :

setoid β

The relation 'in the same orbit'.

Equations

add_action.orbit_rel α β = {r := λ (a b : β), a ∈ add_action.orbit α b, iseqv := _}

source

theorem mul_action.quotient_preimage_image_eq_union_mul {α : Type u} {β : Type v} [group α] [mul_action α β] (U : set β) :

quotient.mk ⁻¹' (quotient.mk '' U) = ⋃ (a : α), has_smul.smul a '' U

When you take a set U in β, push it down to the quotient, and pull back, you get the union of the orbit of U under α.

source

theorem add_action.quotient_preimage_image_eq_union_add {α : Type u} {β : Type v} [add_group α] [add_action α β] (U : set β) :

quotient.mk ⁻¹' (quotient.mk '' U) = ⋃ (a : α), has_vadd.vadd a '' U

When you take a set U in β, push it down to the quotient, and pull back, you get the union of the orbit of U under α.

source

theorem add_action.disjoint_image_image_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] {U V : set β} :

disjoint (quotient.mk '' U) (quotient.mk '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), a +ᵥ x ∉ V

source

theorem mul_action.disjoint_image_image_iff {α : Type u} {β : Type v} [group α] [mul_action α β] {U V : set β} :

disjoint (quotient.mk '' U) (quotient.mk '' V) ↔ ∀ (x : β), x ∈ U → ∀ (a : α), a • x ∉ V

source

theorem add_action.image_inter_image_iff {α : Type u} {β : Type v} [add_group α] [add_action α β] (U V : set β) :

quotient.mk '' U ∩ quotient.mk '' V = ∅ ↔ ∀ (x : β), x ∈ U → ∀ (a : α), a +ᵥ x ∉ V

source

theorem mul_action.image_inter_image_iff {α : Type u} {β : Type v} [group α] [mul_action α β] (U V : set β) :

quotient.mk '' U ∩ quotient.mk '' V = ∅ ↔ ∀ (x : β), x ∈ U → ∀ (a : α), a • x ∉ V

source

@[reducible]

def add_action.orbit_rel.quotient (α : Type u) (β : Type v) [add_group α] [add_action α β] :

Type v

The quotient by add_action.orbit_rel, given a name to enable dot notation.

Equations

add_action.orbit_rel.quotient α β = quotient (add_action.orbit_rel α β)

source

@[reducible]

def mul_action.orbit_rel.quotient (α : Type u) (β : Type v) [group α] [mul_action α β] :

Type v

The quotient by mul_action.orbit_rel, given a name to enable dot notation.

Equations

mul_action.orbit_rel.quotient α β = quotient (mul_action.orbit_rel α β)

source

def mul_action.orbit_rel.quotient.orbit {α : Type u} {β : Type v} [group α] [mul_action α β] (x : mul_action.orbit_rel.quotient α β) :

set β

The orbit corresponding to an element of the quotient by mul_action.orbit_rel

Equations

x.orbit = quotient.lift_on' x (mul_action.orbit α) mul_action.orbit_rel.quotient.orbit._proof_1

source

def add_action.orbit_rel.quotient.orbit {α : Type u} {β : Type v} [add_group α] [add_action α β] (x : add_action.orbit_rel.quotient α β) :

set β

The orbit corresponding to an element of the quotient by add_action.orbit_rel

Equations

x.orbit = quotient.lift_on' x (add_action.orbit α) add_action.orbit_rel.quotient.orbit._proof_1

source

@[simp]

theorem mul_action.orbit_rel.quotient.orbit_mk {α : Type u} {β : Type v} [group α] [mul_action α β] (b : β) :

mul_action.orbit_rel.quotient.orbit (quotient.mk' b) = mul_action.orbit α b

source

@[simp]

theorem add_action.orbit_rel.quotient.orbit_mk {α : Type u} {β : Type v} [add_group α] [add_action α β] (b : β) :

add_action.orbit_rel.quotient.orbit (quotient.mk' b) = add_action.orbit α b

source

theorem add_action.orbit_rel.quotient.mem_orbit {α : Type u} {β : Type v} [add_group α] [add_action α β] {b : β} {x : add_action.orbit_rel.quotient α β} :

b ∈ x.orbit ↔ quotient.mk' b = x

source

theorem mul_action.orbit_rel.quotient.mem_orbit {α : Type u} {β : Type v} [group α] [mul_action α β] {b : β} {x : mul_action.orbit_rel.quotient α β} :

b ∈ x.orbit ↔ quotient.mk' b = x

source

theorem add_action.orbit_rel.quotient.orbit_eq_orbit_out {α : Type u} {β : Type v} [add_group α] [add_action α β] (x : add_action.orbit_rel.quotient α β) {φ : add_action.orbit_rel.quotient α β → β} (hφ : function.right_inverse φ quotient.mk') :

x.orbit = add_action.orbit α (φ x)

Note that hφ = quotient.out_eq' is a useful choice here.

source

theorem mul_action.orbit_rel.quotient.orbit_eq_orbit_out {α : Type u} {β : Type v} [group α] [mul_action α β] (x : mul_action.orbit_rel.quotient α β) {φ : mul_action.orbit_rel.quotient α β → β} (hφ : function.right_inverse φ quotient.mk') :

x.orbit = mul_action.orbit α (φ x)

Note that hφ = quotient.out_eq' is a useful choice here.

source

def mul_action.self_equiv_sigma_orbits' (α : Type u) (β : Type v) [group α] [mul_action α β] :

β ≃ Σ (ω : mul_action.orbit_rel.quotient α β), ↥(ω.orbit)

Decomposition of a type X as a disjoint union of its orbits under a group action.

This version is expressed in terms of mul_action.orbit_rel.quotient.orbit instead of mul_action.orbit, to avoid mentioning quotient.out'.

Equations

mul_action.self_equiv_sigma_orbits' α β = (equiv.sigma_fiber_equiv quotient.mk').symm.trans (equiv.sigma_congr_right (λ (ω : mul_action.orbit_rel.quotient α β), equiv.subtype_equiv_right _))

source

def add_action.self_equiv_sigma_orbits' (α : Type u) (β : Type v) [add_group α] [add_action α β] :

β ≃ Σ (ω : add_action.orbit_rel.quotient α β), ↥(ω.orbit)

Decomposition of a type X as a disjoint union of its orbits under an additive group action.

This version is expressed in terms of add_action.orbit_rel.quotient.orbit instead of add_action.orbit, to avoid mentioning quotient.out'.

Equations

add_action.self_equiv_sigma_orbits' α β = (equiv.sigma_fiber_equiv quotient.mk').symm.trans (equiv.sigma_congr_right (λ (ω : add_action.orbit_rel.quotient α β), equiv.subtype_equiv_right _))

source

def mul_action.self_equiv_sigma_orbits (α : Type u) (β : Type v) [group α] [mul_action α β] :

β ≃ Σ (ω : mul_action.orbit_rel.quotient α β), ↥(mul_action.orbit α (quotient.out' ω))

Decomposition of a type X as a disjoint union of its orbits under a group action.

Equations

mul_action.self_equiv_sigma_orbits α β = (mul_action.self_equiv_sigma_orbits' α β).trans (equiv.sigma_congr_right (λ (i : mul_action.orbit_rel.quotient α β), equiv.set.of_eq _))

source

def add_action.self_equiv_sigma_orbits (α : Type u) (β : Type v) [add_group α] [add_action α β] :

β ≃ Σ (ω : add_action.orbit_rel.quotient α β), ↥(add_action.orbit α (quotient.out' ω))

Decomposition of a type X as a disjoint union of its orbits under an additive group action.

Equations

add_action.self_equiv_sigma_orbits α β = (add_action.self_equiv_sigma_orbits' α β).trans (equiv.sigma_congr_right (λ (i : add_action.orbit_rel.quotient α β), equiv.set.of_eq _))

source

theorem mul_action.stabilizer_smul_eq_stabilizer_map_conj {α : Type u} {β : Type v} [group α] [mul_action α β] (g : α) (x : β) :

mul_action.stabilizer α (g • x) = subgroup.map (mul_equiv.to_monoid_hom (⇑mul_aut.conj g)) (mul_action.stabilizer α x)

If the stabilizer of x is S, then the stabilizer of g • x is gSg⁻¹.

source

noncomputable def mul_action.stabilizer_equiv_stabilizer_of_orbit_rel {α : Type u} {β : Type v} [group α] [mul_action α β] {x y : β} (h : (mul_action.orbit_rel α β).rel x y) :

↥(mul_action.stabilizer α x) ≃* ↥(mul_action.stabilizer α y)

A bijection between the stabilizers of two elements in the same orbit.

Equations

mul_action.stabilizer_equiv_stabilizer_of_orbit_rel h = let g : α := classical.some h in have hg : g • y = x, from _, have this : mul_action.stabilizer α x = subgroup.map (mul_equiv.to_monoid_hom (⇑mul_aut.conj g)) (mul_action.stabilizer α y), from _, (mul_equiv.subgroup_congr this).trans (mul_equiv.subgroup_map (⇑mul_aut.conj g) (mul_action.stabilizer α y)).symm

source

theorem add_action.stabilizer_vadd_eq_stabilizer_map_conj {α : Type u} {β : Type v} [add_group α] [add_action α β] (g : α) (x : β) :

add_action.stabilizer α (g +ᵥ x) = add_subgroup.map (add_equiv.to_add_monoid_hom (⇑add_aut.conj g)) (add_action.stabilizer α x)

If the stabilizer of x is S, then the stabilizer of g +ᵥ x is g + S + (-g).

source

noncomputable def add_action.stabilizer_equiv_stabilizer_of_orbit_rel {α : Type u} {β : Type v} [add_group α] [add_action α β] {x y : β} (h : (add_action.orbit_rel α β).rel x y) :

↥(add_action.stabilizer α x) ≃+ ↥(add_action.stabilizer α y)

A bijection between the stabilizers of two elements in the same orbit.

Equations

add_action.stabilizer_equiv_stabilizer_of_orbit_rel h = let g : α := classical.some h in have hg : g +ᵥ y = x, from _, have this : add_action.stabilizer α x = add_subgroup.map (add_equiv.to_add_monoid_hom (⇑add_aut.conj g)) (add_action.stabilizer α y), from _, (add_equiv.add_subgroup_congr this).trans (add_equiv.add_subgroup_map (⇑add_aut.conj g) (add_action.stabilizer α y)).symm

source

theorem smul_cancel_of_non_zero_divisor {M : Type u_1} {R : Type u_2} [monoid M] [non_unital_non_assoc_ring R] [distrib_mul_action M R] (k : M) (h : ∀ (x : R), k • x = 0 → x = 0) {a b : R} (h' : k • a = k • b) :

a = b

smul by a k : M over a ring is injective, if k is not a zero divisor. The general theory of such k is elaborated by is_smul_regular. The typeclass that restricts all terms of M to have this property is no_zero_smul_divisors.

mathlib documentation

Basic properties of group actions #

Main definitions #