# Why does #check add_mul (R := ℕ) return add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * instead of add_mul : Prop?

I don't understand why #check add_mul (R := ℕ) returns add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c instead of add_mul : prop. In my opinion add_mul (R := ℕ) is a proposition therefore Lean infoview should say add_mul : Prop (clearly I am wrong, and I want to know why).

• Perhaps it's our naming convention that confuses you: since we don't care which element of these types we have, we just name an element after the type, instead of giving names according to the structure of the element.
– Trebor
Commented May 21 at 8:57
• You have two judgements here: the first one is that add_mul : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c and the second one is that ∀ (a b c : ℕ), (a + b) * c = a * c + b * c : Prop Commented May 21 at 13:30

add_mul is a proof of ∀ (a b c : ℕ), (a + b) * c = a * c + b * c, not the proposition itself.
def cat : ∀ (a b c : ℕ), (a + b) * c = a * c + b * c := by ...

The type of cat is ∀ (a b c : ℕ), (a + b) * c = a * c + b * c. The type of dog is Prop.