Documentation
Batteries
.
Data
.
Nat
.
Gcd
Search
return to top
source
Imports
Init
Batteries.Tactic.Alias
Imported by
Nat
.
Coprime
.
mul
Definitions and properties of
coprime
#
source
@[deprecated Nat.Coprime.mul_left (since := "2025-08-04")]
theorem
Nat
.
Coprime
.
mul
{
m
k
n
:
Nat
}
(
H1
:
m
.
Coprime
k
)
(
H2
:
n
.
Coprime
k
)
:
(
m
*
n
).
Coprime
k
Alias
of
Nat.Coprime.mul_left
.