0!

Stream: maths

[Johan Commelin]

Is this intentional? (docs#nat.factorial_zero)

@[simp] theorem factorial_zero : 0! = 1! := rfl

[Adam Topaz]

example : 1 = 1 * 1 := rfl

[Kevin Buzzard]

7*8=56 is rfl, it doesn't mean it's helpful :-)

[Adam Topaz]

I guess it's helpful for the simp?

[Kevin Buzzard]

Four lines later we have

@[simp] theorem factorial_one : 1! = 1 := rfl

so in fact factorial_zero as it stands makes simp take more time, not less.

[Floris van Doorn]

@Anatole Dedecker wrote this originally. I think it makes more sense to change the RHS of factorial_zero to 1, but honestly it doesn't matter much.

[Johan Commelin]

I was just surprised that I needed two lemmas in my simp only

[Anatole Dedecker]

I don't think I wrote this lemma, but I did the change from fact to factorial so git blame probably tells it's me

[Floris van Doorn]

#7697