doc comment of `himp_bot`

Stream: mathlib4

[Asei Inoue]

This is correct? (copy-paste mistake?)

/-- A Heyting algebra is a bounded lattice with an additional binary operation `⇨` called Heyting
implication such that `a ⇨` is right adjoint to `a ⊓`. -/
class HeytingAlgebra (α : Type*) extends GeneralizedHeytingAlgebra α, OrderBot α, HasCompl α where
  /-- `a ⇨` is right adjoint to `a ⊓` -/
  himp_bot (a : α) : a ⇨ ⊥ = aᶜ

[Asei Inoue]

https://github.com/leanprover-community/mathlib4/blob/2969d0119259fdf37a81cca002481be932cc8953/Mathlib/Order/Heyting/Basic.lean#L144

[Yaël Dillies]

Yes, copy-paste error. Feel free to open a PR and request my review!

[Asei Inoue]

done

https://github.com/leanprover-community/mathlib4/pull/16587

[Yury G. Kudryashov]

@Yaël Dillies maintainer merge would be more visible. Delegated.

[Yaël Dillies]

What do you mean? I didn't yet have time to review it

[Yury G. Kudryashov]

Sorry, I misinterpreted your :praise:.