coe_default_Iic_zero
coe_default_Iic_zero🔗
Lemma
coe_default_Iic_zeroNo docstring.
theorem
coe_default_Iic_zero : ↑default = 0coe_default_Iic_zero : ↑default = 0
Code
lemma coe_default_Iic_zero : ((default : Iic 0) : ℕ) = 0
Used by (1)
Actions: Source · Open Issue
Proof
rfl