Documentation
Mathlib
.
GroupTheory
.
Congruence
.
Star
Search
return to top
source
Imports
Init
Mathlib.Algebra.Star.Basic
Mathlib.GroupTheory.Congruence.Basic
Imported by
ConGen
.
Rel
.
star
conGen_star
AddConGen
.
Rel
.
star
addConGen_star
Helpers for working with star operators on quotients.
#
TODO: consider defining
Star
versions of
Con
and
AddCon
.
source
theorem
ConGen
.
Rel
.
star
{
M
:
Type
u_1}
[
Mul
M
]
[
StarMul
M
]
{
r
:
M
→
M
→
Prop
}
(
hr
:
∀ (
a
b
:
M
),
r
a
b
→
r
(
Star.star
a
)
(
Star.star
b
)
)
⦃
a
b
:
M
⦄
:
Rel
r
a
b
→
Rel
r
(
Star.star
a
)
(
Star.star
b
)
source
theorem
conGen_star
{
M
:
Type
u_1}
[
Mul
M
]
[
StarMul
M
]
{
r
:
M
→
M
→
Prop
}
(
hr
:
∀ (
a
b
:
M
),
r
a
b
→
r
(
star
a
)
(
star
b
)
)
⦃
a
b
:
M
⦄
:
(
conGen
r
)
a
b
→
(
conGen
r
)
(
star
a
)
(
star
b
)
source
theorem
AddConGen
.
Rel
.
star
{
A
:
Type
u_1}
[
AddMonoid
A
]
[
StarAddMonoid
A
]
{
r
:
A
→
A
→
Prop
}
(
hr
:
∀ (
a
b
:
A
),
r
a
b
→
r
(
Star.star
a
)
(
Star.star
b
)
)
⦃
a
b
:
A
⦄
:
Rel
r
a
b
→
Rel
r
(
Star.star
a
)
(
Star.star
b
)
source
theorem
addConGen_star
{
A
:
Type
u_1}
[
AddMonoid
A
]
[
StarAddMonoid
A
]
{
r
:
A
→
A
→
Prop
}
(
hr
:
∀ (
a
b
:
A
),
r
a
b
→
r
(
star
a
)
(
star
b
)
)
⦃
a
b
:
A
⦄
:
(
addConGen
r
)
a
b
→
(
addConGen
r
)
(
star
a
)
(
star
b
)